research-article

Public Access

An Architecture Supporting Formal and Compositional Binary Analysis

Authors:

Joseph McMahan,

Michael Christensen,

Lawton Nichols,

Timothy SherwoodAuthors Info & Claims

ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems

Pages 177 - 191

https://doi.org/10.1145/3037697.3037733

Published: 04 April 2017 Publication History

Abstract

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

References

[1]

The Coq proof assistant: https://coq.inria.fr.

[2]

How many people have ICDs? http://asktheicd.com/tile/106/english-implantable-cardioverter-defibrillator-icd/how-many-people-have-icds/.

[3]

Living with your implantable cardioverter defibrillator (ICD). http://www.heart.org/HEARTORG/Conditions/Arrhythmia/PreventionTreatmentofArrhythmia/Living-With-Your-Implantable-Cardioverter-Defibrillator-ICD_UCM_448462_Article.jsp.

[4]

Open source ECG analysis software. http://www.eplimited.com/confirmation.htm.

[5]

Journal of Automated Reasoning, 30(3--4), 2003.

[6]

M. Abadi, A. Banerjee, N. Heintze, and J. G. Riecke. A core calculus of dependency. In Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '99, pages 147--160, New York, NY, USA, 1999. ACM.

Digital Library

[7]

A. W. Appel. Foundational proof-carrying code. In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science, LICS '01, pages 247--, Washington, DC, USA, 2001. IEEE Computer Society.

[8]

A. W. Appel. Verified software toolchain. In Proceedings of the 20th European Conference on Programming Languages and Systems: Part of the Joint European Conferences on Theory and Practice of Software, ESOP'11/ETAPS'11, pages 1--17, Berlin, Heidelberg, 2011. Springer-Verlag.

[9]

M. Barnett, B.-Y. E. Chang, R. DeLine, B. Jacobs, and K. R. M. Leino. Boogie: A modular reusable verifier for object-oriented programs. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO'05, pages 364--387, Berlin, Heidelberg, 2006. Springer-Verlag.

Digital Library

[10]

R. S. Boyer and Y. Yu. Automated correctness proofs of machine code programs for a commercial microprocessor. In Proceedings of the 11th International Conference on Automated Deduction: Automated Deduction, CADE-11, pages 416--430, London, UK, UK, 1992. Springer-Verlag.

[11]

T. Chen, M. Diciolla, M. Kwiatkowska, and A. Mereacre. Quantitative verification of implantable cardiac pacemakers. In Real-Time Systems Symposium (RTSS), 2012 IEEE 33rd, pages 263--272. IEEE, 2012.

Digital Library

[12]

A. Chlipala. A verified compiler for an impure functional language. In ACM Sigplan Notices, volume 45, pages 93--106. ACM, 2010.

Digital Library

[13]

A. Chlipala. Mostly-automated verification of low-level programs in computational separation logic. In Proceedings of the 32Nd ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '11, pages 234--245, New York, NY, USA, 2011. ACM.

Digital Library

[14]

T. J. Clarke, P. J. Gladstone, C. D. MacLean, and A. C. Norman. Skim - the s, k, i reduction machine. In Proceedings of the 1980 ACM Conference on LISP and Functional Programming, LFP '80, pages 128--135, New York, NY, USA, 1980. ACM.

Digital Library

[15]

S. J. Connolly, M. Gent, R. S. Roberts, P. Dorian, D. Roy, R. S. Sheldon, L. B. Mitchell, M. S. Green, G. J. Klein, and B. O\textquoterightBrien. Canadian implantable defibrillator study (cids). Circulation, 101(11):1297--1302, 2000.

[16]

M. E. Conway. Design of a separable transition-diagram compiler. Commun. ACM, 6(7):396--408, July 1963.

Digital Library

[17]

L. C. Cordeiro, B. Fischer, H. Chen, and J. Marques-Silva. Semiformal verification of embedded software in medical devices considering stringent hardware constraints. In ICESS, 2009.

Digital Library

[18]

M. M. Cruz-Cunha, J. Varajão, H. Krcmar, R. Martinho, R. A. Álvarez, A. J. M. Penín, and X. A. V. Sobrino. Centeris 2013 - conference on enterprise information systems / projman 2013 - international conference on project management/ hcist 2013 - international conference on health and social care information systems and technologies a comparison of three qrs detection algorithms over a public database. Procedia Technology, 9:1159 -- 1165, 2013.

[19]

P. Curzon and P. Curzon. A verified compiler for a structured assembly language. In In proceedings of the 1991 international workshop on the HOL theorem Proving System and its applications. IEEE Computer, 1991.

[20]

D. E. Denning and P. J. Denning. Certification of programs for secure information flow. Commun. ACM, 20(7):504--513, July 1977.

Digital Library

[21]

T. Denning, K. Fu, and T. Kohno. Absence makes the heart grow fonder: New directions for implantable medical device security. In HotSec, 2008.

Digital Library

[22]

L. P. Deutsch. A lisp machine with very compact programs. In Proceedings of the 3rd international joint conference on Artificial intelligence, pages 697--703. Morgan Kaufmann Publishers Inc., 1973.

Digital Library

[23]

A. Fox and M. O. Myreen. A trustworthy monadic formalization of the armv7 instruction set architecture. In Proceedings of the First International Conference on Interactive Theorem Proving, ITP'10, pages 243--258, Berlin, Heidelberg, 2010. Springer-Verlag.

Digital Library

[24]

J. A. Goguen and J. Meseguer. Security policies and security models. In Security and Privacy, 1982 IEEE Symposium on, pages 11--11, April 1982.

[25]

S. Gollakota, H. Hassanieh, B. Ransford, D. Katabi, and K. Fu. They can hear your heartbeats: non-invasive security for implantable medical devices. In Proc. ACM Conf. SIGCOMM, pages 2--13, 2011.

Digital Library

[26]

A. O. Gomes and M. V. M. Oliveira. Formal Specification of a Cardiac Pacing System, pages 692--707. Springer Berlin Heidelberg, Berlin, Heidelberg, 2009.

[27]

B. Graham. Secd: Design issues. Technical report, University of Calgary, 1989.

[28]

D. Halperin, T. S. Heydt-Benjamin, B. Ransford, S. S. Clark, B. Defend, W. Morgan, K. Fu, T. Kohno, and W. H. Maisel. Pacemakers and implantable cardiac defibrillators: Software radio attacks and zero-power defenses. In 2008 IEEE Symposium on Security and Privacy (sp 2008), pages 129--142. IEEE, 2008.

Digital Library

[29]

B. Hardekopf and C. Lin. Flow-sensitive pointer analysis for millions of lines of code. In Proceedings of the 9th Annual IEEE/ACM International Symposium on Code Generation and Optimization, CGO '11, pages 289--298, Washington, DC, USA, 2011. IEEE Computer Society.

[30]

N. Heintze and J. G. Riecke. The slam calculus: Programming with secrecy and integrity. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '98, pages 365--377, New York, NY, USA, 1998. ACM.

Digital Library

[31]

R. Hindley. The principal type-scheme of an object in combinatory logic. Transactions of the American Mathematical Society, 146:29--60, 1969.

[32]

P. Hudak, J. Hughes, S. Peyton Jones, and P. Wadler. A history of haskell: being lazy with class. In Proceedings of the third ACM SIGPLAN conference on History of programming languages, pages 12--1. ACM, 2007.

Digital Library

[33]

W. A. Hunt Jr. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429--460, 1989.

Digital Library

[34]

Z. Jiang, M. Pajic, and R. Mangharam. Cyber-physical modeling of implantable cardiac medical devices. Proceedings of the IEEE, 100(1):122--137, Jan 2012.

[35]

V. Kashyap, B. Wiedermann, and B. Hardekopf. Timing- and termination-sensitive secure information flow: Exploring a new approach. In 2011 IEEE Symposium on Security and Privacy, pages 413--428, May 2011.

Digital Library

[36]

E. Keller, J. Szefer, J. Rexford, and R. B. Lee. Nohype: Virtualized cloud infrastructure without the virtualization. SIGARCH Comput. Archit. News, 38(3):350--361, June 2010.

Digital Library

[37]

A. Kennedy, N. Benton, J. B. Jensen, and P.-E. Dagand. Coq: The world's best macro assembler? In Proceedings of the 15th Symposium on Principles and Practice of Declarative Programming, PPDP '13, pages 13--24, New York, NY, USA, 2013. ACM.

Digital Library

[38]

G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, et al. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles, pages 207--220. ACM, 2009.

Digital Library

[39]

T. F. Knight. Implementation of a list processing machine. PhD thesis, Massachusetts Institute of Technology, 1979.

[40]

P. M. Kogge. "The Architecture of Symbolic Computers". McGraw-Hill, Inc., New York, New York, 1991.

[41]

P. J. Landin. The Mechanical Evaluation of Expressions. The Computer Journal, 6(4):308--320, Jan. 1964.

[42]

X. Leroy. A formally verified compiler back-end. Journal of Automated Reasoning, 43(4):363--446, 2009.

Digital Library

[43]

T. Maeda and A. Yonezawa. Typed assembly language for implementing os kernels in smp/multi-core environments with interrupts. In Proceedings of the 5th International Conference on Systems Software Verification, SSV'10, pages 1--1, Berkeley, CA, USA, 2010. USENIX Association.

Digital Library

[44]

R. Mangharam, H. Abbas, M. Behl, K. Jang, M. Pajic, and Z. Jiang. Three challenges in cyber-physical systems. In 2016 8th International Conference on Communication Systems and Networks (COMSNETS), pages 1--8, Jan 2016.

[45]

J. M. McCune, B. J. Parno, A. Perrig, M. K. Reiter, and H. Isozaki. Flicker: An execution infrastructure for tcb minimization. SIGOPS Oper. Syst. Rev., 42(4):315--328, Apr. 2008.

Digital Library

[46]

N. G. Michael and A. W. Appel. Machine instruction syntax and semantics in higher order logic. In Proceedings of the 17th International Conference on Automated Deduction, CADE-17, pages 7--24, London, UK, UK, 2000. Springer-Verlag.

[47]

R. Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348--375, 1978.

[48]

E. Moggi. Notions of computation and monads. Information and computation, 93(1):55--92, 1991.

Digital Library

[49]

J. S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461--492, 1989.

Digital Library

[50]

A. L. D. Moura and R. Ierusalimschy. Revisiting coroutines. ACM Trans. Program. Lang. Syst., 31(2):6:1--6:31, Feb. 2009.

Digital Library

[51]

G. C. Necula. Translation validation for an optimizing compiler. In ACM sigplan notices, volume 35, pages 83--94. ACM, 2000.

Digital Library

[52]

G. C. Necula. Proof-carrying code. design and implementation. Springer, 2002.

[53]

G. Neis, C.-K. Hur, J.-O. Kaiser, C. McLaughlin, D. Dreyer, and V. Vafeiadis. Pilsner: A compositionally verified compiler for a higher-order imperative language. In Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming, ICFP 2015, pages 166--178, New York, NY, USA, 2015. ACM.

Digital Library

[54]

J. Pan and W. J. Tompkins. A real-time qrs detection algorithm. IEEE Transactions on Biomedical Engineering, BME-32(3):230--236, March 1985.

[55]

F. Pottier and V. Simonet. Information flow inference for ml. ACM Trans. Program. Lang. Syst., 25(1):117--158, Jan. 2003.

Digital Library

[56]

T. Ramananandro, Z. Shao, S.-C. Weng, J. Koenig, and Y. Fu. A compositional semantics for verified separate compilation and linking. In Proceedings of the 2015 Conference on Certified Programs and Proofs, CPP '15, pages 3--14, New York, NY, USA, 2015. ACM.

Digital Library

[57]

J. M. Rushby. Proof of separability: A verification technique for a class of a security kernels. In Proceedings of the 5th Colloquium on International Symposium on Programming, pages 352--367, London, UK, UK, 1982. Springer-Verlag.

[58]

A. Sabelfeld and A. C. Myers. Language-based information-flow security. IEEE J.Sel. A. Commun., 21(1):5--19, Sept. 2006.

Digital Library

[59]

S. Shuja, S. K. Srinivasan, S. Jabeen, and D. Nawarathna. A formal verification methodology for ddd mode pacemaker control programs. Journal of Electrical and Computer Engineering, 2015.

Digital Library

[60]

J. Siebels, K.-H. Kuck, and C. Investigators. Implantable cardioverter defibrillator compared with antiarrhythmic drug treatment in cardiac arrest survivors (the cardiac arrest study hamburg). American Heart Journal, 127:1139--1144, April 1994.

[61]

V. Simonet. Fine-grained information flow analysis for a $łambda$ calculus with sum types. In Proceedings of the 15th IEEE Workshop on Computer Security Foundations, CSFW '02, pages 223--, Washington, DC, USA, 2002. IEEE Computer Society.

[62]

M. Strecker. Formal verification of a java compiler in isabelle. In Automated Deduction-CADE-18, pages 63--77. Springer, 2002.

[63]

D. Terei, S. Marlow, S. Peyton Jones, and D. Mazières. Safe haskell. In Proceedings of the 2012 Haskell Symposium, Haskell '12, pages 137--148, New York, NY, USA, 2012. ACM.

Digital Library

[64]

H. Tuch, G. Klein, and M. Norrish. Types, bytes, and separation logic. In Martin Hofmann and Matthias Felleisen, editor, ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 97--108, Nice, France, jan 2007. ACM.

Digital Library

[65]

T. A. versus Implantable Defibrillators (AVID) Investigators. A comparison of antiarrhythmic-drug therapy with implantable defibrillators in patients resuscitated from near-fatal ventricular arrhythmias. New England Journal of Medicine, 337(22):1576--1584, 1997. 9411221.

[66]

D. Volpano, C. Irvine, and G. Smith. A sound type system for secure flow analysis. J. Comput. Secur., 4(2--3):167--187, Jan. 1996.

Digital Library

[67]

M. S. Wathen, P. J. DeGroot, M. O. Sweeney, A. J. Stark, M. F. Otterness, W. O. Adkisson, R. C. Canby, K. Khalighi, C. Machado, D. S. Rubenstein, and K. J. Volosin. Prospective randomized multicenter trial of empirical antitachycardia pacing versus shocks for spontaneous rapid ventricular tachycardia in patients with implantable cardioverter-defibrillators. Circulation, 110(17):2591--2596, 2004.

[68]

H. Xi and R. Harper. A dependently typed assembly language. In ACM SIGPLAN Notices, volume 36, pages 169--180. ACM, 2001.

Digital Library

[69]

J. Yang and C. Hawblitzel. Safe to the last instruction: Automated verification of a type-safe operating system. In Proceedings of the 31st ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI '10, pages 99--110, New York, NY, USA, 2010. ACM.

Digital Library

[70]

D. Yu, N. A. Hamid, and Z. Shao. Building certified libraries for pcc: dynamic storage allocation. In Proceedings of the 12th European conference on Programming, pages 363--379. Springer-Verlag, 2003.

Cited By

Accetti CLiu P(2022)Architectural Support for Functional Programming2022 IFIP/IEEE 30th International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC54400.2022.9939644(1-2)Online publication date: 3-Oct-2022
https://doi.org/10.1109/VLSI-SoC54400.2022.9939644
Accetti CYing RLiu P(2022)Structured Combinators for Efficient Graph ReductionIEEE Computer Architecture Letters10.1109/LCA.2022.319884421:2(73-76)Online publication date: 1-Jul-2022
https://doi.org/10.1109/LCA.2022.3198844
Melo CLiu PYing R(2020)A Platform for Full-Stack Functional Programming2020 IEEE International Symposium on Circuits and Systems (ISCAS)10.1109/ISCAS45731.2020.9180772(1-5)Online publication date: Oct-2020
https://doi.org/10.1109/ISCAS45731.2020.9180772
Show More Cited By

Index Terms

An Architecture Supporting Formal and Compositional Binary Analysis

Recommendations

An Architecture Supporting Formal and Compositional Binary Analysis
ASPLOS '17

Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation. Rather than trying to analyze complete binaries and the countless ways ...
An Architecture Supporting Formal and Compositional Binary Analysis
Asplos'17

Building a trustworthy life-critical embedded system requires deep reasoning about the potential effects that sequences of machine instructions can have on full system operation. Rather than trying to analyze complete binaries and the countless ways ...
Reference count analysis with shallow aliasing

Reference counting is a commonly used technique for resource management. One key correctness criterion in the use of reference counts is that increment and decrement operations must be well-matched. In this paper we consider the problem of statically ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating Systems

April 2017

856 pages

ISBN:9781450344654

DOI:10.1145/3037697

General Chairs:
Yunji Chen
Institute of Computing Technology, CAS, China
,
Olivier Temam
Google, USA
,
Program Chair:
John Carter
IBM, USA

ACM SIGPLAN Notices Volume 52, Issue 4
ASPLOS '17
April 2017
811 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/3093336
Editor:
Matthew Fluet
Issue’s Table of Contents
ACM SIGARCH Computer Architecture News Volume 45, Issue 1
Asplos'17
March 2017
812 pages
ISSN:0163-5964
DOI:10.1145/3093337
Editor:
Babak Falsafi
Interim
Issue’s Table of Contents

Copyright © 2017 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Sponsors

In-Cooperation

SIGBED: ACM Special Interest Group on Embedded Systems

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 04 April 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

NSF

Conference

ASPLOS '17

Sponsor:

ASPLOS '17: Architectural Support for Programming Languages and Operating Systems

April 8 - 12, 2017

Xi'an, China

Acceptance Rates

ASPLOS '17 Paper Acceptance Rate 53 of 320 submissions, 17%;

Overall Acceptance Rate 535 of 2,713 submissions, 20%

Upcoming Conference

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

6
Total Citations
View Citations
790
Total Downloads

Downloads (Last 12 months)177
Downloads (Last 6 weeks)11

Reflects downloads up to 13 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Accetti CLiu P(2022)Architectural Support for Functional Programming2022 IFIP/IEEE 30th International Conference on Very Large Scale Integration (VLSI-SoC)10.1109/VLSI-SoC54400.2022.9939644(1-2)Online publication date: 3-Oct-2022
https://doi.org/10.1109/VLSI-SoC54400.2022.9939644
Accetti CYing RLiu P(2022)Structured Combinators for Efficient Graph ReductionIEEE Computer Architecture Letters10.1109/LCA.2022.319884421:2(73-76)Online publication date: 1-Jul-2022
https://doi.org/10.1109/LCA.2022.3198844
Melo CLiu PYing R(2020)A Platform for Full-Stack Functional Programming2020 IEEE International Symposium on Circuits and Systems (ISCAS)10.1109/ISCAS45731.2020.9180772(1-5)Online publication date: Oct-2020
https://doi.org/10.1109/ISCAS45731.2020.9180772
McMahan JChristensen MDewey KHardekopf BSherwood TManne SHunter HAltman E(2019)BouncerProceedings of the 46th International Symposium on Computer Architecture10.1145/3307650.3322256(711-722)Online publication date: 22-Jun-2019
https://dl.acm.org/doi/10.1145/3307650.3322256
Clow JTzimpragos GDangwal DGuo SMcMahan JSherwood T(2017)A pythonic approach for rapid hardware prototyping and instrumentation2017 27th International Conference on Field Programmable Logic and Applications (FPL)10.23919/FPL.2017.8056860(1-7)Online publication date: Sep-2017
https://doi.org/10.23919/FPL.2017.8056860
Christensen MMcMahan JNichols LRoesch JHardekopf BSherwood T(2020)Safe Functional Systems through Integrity Types and Verified AssemblyTheoretical Computer Science10.1016/j.tcs.2020.09.039Online publication date: Sep-2020
https://doi.org/10.1016/j.tcs.2020.09.039

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

Media

Figures

Other

Tables

View Table of Contents