An Architecture Supporting Formal and Compositional Binary Analysis

摘要: Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full operation. Rather than trying to analyze complete binaries and countless ways their interact with one another --- memory, side effects, control registers, implicit state, etc. we explore new approach. We propose an architecture controlled by thin computational layer designed tightly correspond lambda calculus, drawing principles functional programming bring assembly much closer myriad frameworks, such as Coq proof assistant. This approach allows assembly-level verified versions critical code operate safely in tandem arbitrary code, including imperative unverified components, without need for large supporting trusted computing bases. demonstrate this be built way simultaneously provide programmability compact, precise, semantics, while still using hardware resources comparable normal systems. To practicality approach, our FPGA-implemented prototype runs medical application which monitors treats life-threatening arrhythmias. Though integrates untrusted formal verification multiple properties end-to-end system, correctness implementation core algorithm, integrity data via non-interference proof, guarantee meets timing requirements.