An Architecture Supporting Formal and Compositional Binary Analysis
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.
[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.
[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.
[12]
A. Chlipala. A verified compiler for an impure functional language. In ACM Sigplan Notices, volume 45, pages 93--106. ACM, 2010.
[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.
[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.
[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.
[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.
[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.
[21]
T. Denning, K. Fu, and T. Kohno. Absence makes the heart grow fonder: New directions for implantable medical device security. In HotSec, 2008.
[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.
[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.
[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.
[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.
[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.
[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.
[33]
W. A. Hunt Jr. Microprocessor design verification. Journal of Automated Reasoning, 5(4):429--460, 1989.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[49]
J. S. Moore. A mechanically verified language implementation. Journal of Automated Reasoning, 5(4):461--492, 1989.
[50]
A. L. D. Moura and R. Ierusalimschy. Revisiting coroutines. ACM Trans. Program. Lang. Syst., 31(2):6:1--6:31, Feb. 2009.
[51]
G. C. Necula. Translation validation for an optimizing compiler. In ACM sigplan notices, volume 35, pages 83--94. ACM, 2000.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
[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.
Index Terms
- An Architecture Supporting Formal and Compositional Binary Analysis
Recommendations
An Architecture Supporting Formal and Compositional Binary Analysis
ASPLOS '17: Proceedings of the Twenty-Second International Conference on Architectural Support for Programming Languages and Operating SystemsBuilding 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'17Building 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
April 2017
811 pages
April 2017856 pagesISBN:9781450344654DOI:10.1145/3037697- General Chairs:
- Yunji Chen,
- Olivier Temam,
- Program Chair:
- John Carter
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]
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 04 April 2017
Published in SIGPLAN Volume 52, Issue 4
Check for updates
Author Tags
Qualifiers
- Research-article
Funding Sources
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- View Citations6Total Citations
- 790Total Downloads
- Downloads (Last 12 months)177
- Downloads (Last 6 weeks)11
Reflects downloads up to 13 Nov 2024
Other Metrics
Citations
View Options
Get Access
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in