An Architecture for Analysis

We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming to bring the assembly much closer to myriad reasoning frameworks and specification languages. This approach allows assembly-lev...

Full description

Saved in:
Bibliographic Details
Published in:IEEE MICRO 2018-05, Vol.38 (3), p.107-115
Main Authors: McMahan, Joseph, Christensen, Michael, Nichols, Lawton, Roesch, Jared, Guo, Sung-Yee, Hardekopf, Ben, Sherwood, Timothy
Format: Article
Language:English
Subjects:
Architecture
Assembly
binary analysis
Calculus
Computer architecture
embedded systems
Functional programming
hardware
Magnetic heads
Pattern matching
Software development managemnet
Specification and description languages
verification
Citations: Items that this one cites
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We propose an architecture controlled by a thin computational layer designed to tightly correspond with the lambda calculus, drawing on principles of functional programming to bring the assembly much closer to myriad reasoning frameworks and specification languages. This approach allows assembly-level verified versions of critical code to operate safely in tandem with arbitrary code without the need for large supporting trusted computing bases.
ISSN:0272-1732
1937-4143
DOI:10.1109/MM.2018.032271067