research-article

Automating Information Flow Analysis of Low Level Code

Authors:

Roberto GuancialeAuthors Info & Claims

CCS '14: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security

Pages 1080 - 1091

https://doi.org/10.1145/2660267.2660322

Published: 03 November 2014 Publication History

Abstract

Low level code is challenging: It lacks structure, it uses jumps and symbolic addresses, the control flow is often highly optimized, and registers and memory locations may be reused in ways that make typing extremely challenging. Information flow properties create additional complications: They are hyperproperties relating multiple executions, and the possibility of interrupts and concurrency, and use of devices and features like memory-mapped I/O requires a departure from the usual initial-state final-state account of noninterference. In this work we propose a novel approach to relational verification for machine code. Verification goals are expressed as equivalence of traces decorated with observation points. Relational verification conditions are propagated between observation points using symbolic execution, and discharged using first-order reasoning. We have implemented an automated tool that integrates with SMT solvers to automate the verification task. The tool transforms ARMv7 binaries into an intermediate, architecture-independent format using the BAP toolset by means of a verified translator. We demonstrate the capabilities of the tool on a separation kernel system call handler, which mixes hand-written assembly with gcc-optimized output, a UART device driver and a crypto service modular exponentiation routine.

References

[1]

O. Aciicmez and Cetin Kaya Koç. Microarchitectural attacks and countermeasures. In Cryptographic Engineering, pages 475--504. 2009.

[2]

J. Agat. Transforming out timing leaks. In POPL, pages 40--53, 2000.

Digital Library

[3]

E. Alkassar, M. A. Hillebrand, S. Knapp, R. Rusev, and S. Tverdyshev. Formal device and programming model for a serial interface. In VERIFY, 2007.

[4]

ARMv7-A architecture reference manual.

[5]

T. Avgerinos, S. K. Cha, B. L. T. Hao, and D. Brumley. Aeg: Automatic exploit generation. In NDSS, 2011.

[6]

G. Balakrishnan and T. Reps. Wysinwyx: What you see is not what you execute. ACM Trans. Program. Lang. Syst., 32:23:1--23:84, August 2010.

Digital Library

[7]

M. Balliu, M. Dam, and G. L. Guernic. Epistemic Temporal Logic for Information Flow Security. In Proceedings of the ACM SIGPLAN Programming Languages and Analysis for Security, june 2011.

Digital Library

[8]

M. Balliu, M. Dam, and G. L. Guernic. ENCoVer: Symbolic Exploration for Information Flow Security. In Proceedings of the IEEE Computer Security Foundations Symposium, pages 30--44, june 2012.

Digital Library

[9]

M. Barnett and K. R. M. Leino. Weakest-precondition of unstructured programs. In PASTE, pages 82--87, 2005.

Digital Library

[10]

G. Barthe, J. M. Crespo, and C. Kunz. Relational verification using product programs. In FM, pages 200--214, 2011.

Digital Library

[11]

G. Barthe, P. R. D'Argenio, and T. Rezk. Secure information flow by self-composition. Mathematical Structures in Computer Science, 21(6):1207--1252, 2011.

Digital Library

[12]

G. Barthe, D. Pichardie, and T. Rezk. A certified lightweight non-interference java bytecode verifier. In Proceedings of the 16th European Conference on Programming, ESOP'07, pages 125--140, Berlin, Heidelberg, 2007. Springer-Verlag.

Digital Library

[13]

J. Brown and T. F. Knight Jr. A minimal trusted computing base for dynamically ensuring secure information flow. 2001.

[14]

D. Brumley, I. Jager, T. Avgerinos, and E. J. Schwartz. Bap: A binary analysis platform. In CAV, pages 463--469, 2011.

Digital Library

[15]

D. Brumley, I. Jager, E. J. Schwartz, and S. Whitman. The bap handbook. http://bap.ece.cmu.edu/doc/bap.pdf, October 2013.

[16]

D. Brumley, H. Wang, S. Jha, and D. X. Song. Creating vulnerability signatures using weakest preconditions. In CSF, pages 311--325, 2007.

Digital Library

[17]

D. Caselden, A. Bazhanyuk, M. Payer, S. McCamant, and D. Song. Hi-cfg: Construction by binary analysis and application to attack polymorphism. In ESORICS, pages 164{181, 2013.

[18]

S. K. Cha, T. Avgerinos, A. Rebert, and D. Brumley. Unleashing mayhem on binary code. In IEEE Symposium on Security and Privacy, pages 380--394, 2012.

Digital Library

[19]

M. Dam, R. Guanciale, N. Khakpour, H. Nemati, and O. Schwarz. Formal verification of information flow security for a simple arm-based separation kernel. In ACM Conference on Computer and Communications Security, pages 223--234, 2013.

Digital Library

[20]

M. Dam, R. Guanciale, and H. Nemati. Machine code verification of a tiny arm hypervisor. In TrustED@CCS, pages 3--12, 2013.

Digital Library

[21]

A. A. de Amorim, N. Collins, A. DeHon, D. Demange, C. Hritcu, D. Pichardie, B. C. Pierce, R. Pollack, and A. Tolmach. A verified information-flow architecture. In POPL, pages 165--178, 2014.

Digital Library

[22]

E. W. Dijkstra. Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM, 18(8):453--457, Aug. 1975.

Digital Library

[23]

J. Duan and J. Regehr. Correctness proofs for device drivers in embedded systems. In Proceedings of the 5th International Conference on Systems Software Verification, SSV'10, pages 5--5, Berkeley, CA, USA, 2010. USENIX Association.

Digital Library

[24]

V. Ganesh and D. L. Dill. A decision procedure for bit-vectors and arrays. In Proc. CAV'07, volume 4590 of Lecture Notes in Computer Science, pages 519--531. Springer, 2007.

Digital Library

[25]

J. A. Goguen and J. Meseguer. Security policies and security models. In Proc. IEEE Symp. on Security and Privacy, pages 11--20, Los Alamitos, Calif., 1982. IEEE Comp. Soc. Press.

[26]

D. Hedin and D. Sands. Timing aware information flow security for a javacard-like bytecode. Electr. Notes Theor. Comput. Sci., 141(1):163--182, 2005.

Digital Library

[27]

C. L. Heitmeyer, M. Archer, E. I. Leonard, and J. Mclean. Formal specification and verification of data separation in a separation kernel for an embedded system. In CCS, pages 346--355. ACM, 2006.

Digital Library

[28]

HOL4. http://hol.sourceforge.net/.

[29]

C. Hritcu, M. Greenberg, B. Karel, B. C. Pierce, and G. Morrisett. All your ifcexception are belong to us. In IEEE Symposium on Security and Privacy, pages 3--17, 2013.

Digital Library

[30]

M. Kovacs, H. Seidl, and B. Finkbeiner. Relational abstract interpretation for the verification of 2-hypersafety properties. In ACM Conference on Computer and Communications Security, pages 211--222, 2013.

Digital Library

[31]

G. Le Guernic. Confidentiality Enforcement Using Dynamic Information Flow Analyses. PhD thesis, Kansas State University, 2007.

Digital Library

[32]

J. McLean. Proving noninterference and functional correctness using traces. Journal of Computer Security, 1(1):37--58, 1992.

Digital Library

[33]

R. Medel, A. Compagnoni, and E. Bonelli. A typed assembly language for non-interference. In Proceedings of the 9th Italian Conference on Theoretical Computer Science, ICTCS'05, pages 360--374. Springer-Verlag, 2005.

Digital Library

[34]

D. Molnar, M. Piotrowski, D. Schultz, and D. Wagner. The program counter security model: Automatic detection and removal of control-flow side channel attacks. In ICISC, pages 156{168, 2005.

Digital Library

[35]

D. Monniaux. Verification of device drivers and intelligent controllers: a case study. In EMSOFT, pages 30--36, 2007.

Digital Library

[36]

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein. Noninterference for operating system kernels. In CPP, pages 126--142, 2012.

Digital Library

[37]

J. Newsome and D. X. Song. Dynamic taint analysis for automatic detection, analysis, and signaturegeneration of exploits on commodity software. In NDSS, 2005.

[38]

N. Partush and E. Yahav. Abstract semantic differencing for numerical programs. In SAS, pages 238--258, 2013.

[39]

D. A. Ramos and D. R. Engler. Practical, low-effort equivalence verification of real code. In CAV, pages 669--685, 2011.

Digital Library

[40]

T. W. Reps, J. Lim, A. V. Thakur, G. Balakrishnan, and A. Lal. There's plenty of room at the bottom: Analyzing and verifying machine code. In CAV, pages 41--56, 2010.

Digital Library

[41]

R. Richards. Modeling and security analysis of a commercial real-time operating system kernel. In D. S. Hardin, editor, Design and Verification of Microprocessor Systems for High-Assurance Applications, pages 301--322. Springer US, 2010.

[42]

A. Sabelfeld and A. Myers. Language-based information-flow security. IEEE J. on Selected Areas in Communications, 21(1):5--19, 2003.

Digital Library

[43]

P. Saxena, P. Poosankam, S. McCamant, and D. Song. Loop-extended symbolic execution on binary programs. In ISSTA, pages 225--236, 2009.

Digital Library

[44]

R. Sharma, E. Schkufza, B. R. Churchill, and A. Aiken. Data-driven equivalence checking. In OOPSLA, pages 391--406, 2013.

Digital Library

[45]

D. Song, D. Brumley, H. Yin, J. Caballero, I. Jager, M. G. Kang, Z. Liang, J. Newsome, P. Poosankam, and P. Saxena. BitBlaze: A new approach to computer security via binary analysis. In Proceedings of the 4th International Conference on Information Systems Security. Keynote invited paper., Hyderabad, India, Dec. 2008.

Digital Library

[46]

G. E. Suh, J. W. Lee, D. Zhang, and S. Devadas. Secure program execution via dynamic information flow tracking. In ACM SIGOPS Operating Systems Review, volume 38, pages 85--96. ACM, 2004.

Digital Library

[47]

T. Terauchi and A. Aiken. Secure information flow as a safety problem. In SAS, pages 352--367, 2005.

Digital Library

[48]

A. V. Thakur, J. Lim, A. Lal, A. Burton, E. Driscoll, M. Elder, T. Andersen, and T. W. Reps. Directed proof generation for machine code. In CAV, pages 288--305, 2010.

Digital Library

[49]

D. Zhang, A. Askarov, and A. C. Myers. Language-based control and mitigation of timing channels. In PLDI, pages 99--110, 2012.

Digital Library

Cited By

Rao XSun CZeng DHuang YTan G(2025)Sliver: A Scalable Slicing-Based Verification for Information Flow SecurityIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2024.340365322:1(457-473)Online publication date: Jan-2025
https://doi.org/10.1109/TDSC.2024.3403653
Soares LCanesche MPereira F(2023)Side-channel Elimination via Partial Control-flow LinearizationACM Transactions on Programming Languages and Systems10.1145/359473645:2(1-43)Online publication date: 26-Jun-2023
https://dl.acm.org/doi/10.1145/3594736
Daniel LBardin SRezk T(2023)Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-ErasureACM Transactions on Privacy and Security10.1145/356303726:2(1-42)Online publication date: 14-Apr-2023
https://dl.acm.org/doi/10.1145/3563037
Show More Cited By

Index Terms

Automating Information Flow Analysis of Low Level Code

Recommendations

Formal verification of information flow security for a simple arm-based separation kernel
CCS '13: Proceedings of the 2013 ACM SIGSAC conference on Computer & communications security

A separation kernel simulates a distributed environment using a single physical machine by executing partitions in isolation and appropriately controlling communication among them. We present a formal verification of information flow security for a ...
Automatic formal verification for scheduled VLIW code

VLIW processors are attractive for many embedded applications, but VLIW code scheduling, whether by hand or by compiler, is extremely challenging. In this paper, we extend previous work on automated verification of low-level software to handle the ...
Automatic formal verification for scheduled VLIW code
LCTES/SCOPES '02: Proceedings of the joint conference on Languages, compilers and tools for embedded systems: software and compilers for embedded systems

VLIW processors are attractive for many embedded applications, but VLIW code scheduling, whether by hand or by compiler, is extremely challenging. In this paper, we extend previous work on automated verification of low-level software to handle the ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

CCS '14: Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security

November 2014

1592 pages

ISBN:9781450329576

DOI:10.1145/2660267

General Chair:
Gail-Joon Ahn
Arizona State University, USA
,
Program Chairs:
Moti Yung
Google -- Columbia University, USA
,
Ninghui Li
Purdue University, USA

Copyright © 2014 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 the author(s) 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

SIGSAC: ACM Special Interest Group on Security, Audit, and Control

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 03 November 2014

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Research-article

Funding Sources

Swedish Foundation for Strategic Research

Conference

CCS'14

Sponsor:

SIGSAC

CCS'14: 2014 ACM SIGSAC Conference on Computer and Communications Security

November 3 - 7, 2014

Arizona, Scottsdale, USA

Acceptance Rates

CCS '14 Paper Acceptance Rate 114 of 585 submissions, 19%;

Overall Acceptance Rate 1,261 of 6,999 submissions, 18%

Upcoming Conference

CCS '25

Sponsor:
sigsac

ACM SIGSAC Conference on Computer and Communications Security

October 13 - 17, 2025

Taipei , Taiwan

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

28
Total Citations
View Citations
603
Total Downloads

Downloads (Last 12 months)28
Downloads (Last 6 weeks)6

Reflects downloads up to 19 Feb 2025

Other Metrics

View Author Metrics

Citations

Cited By

Rao XSun CZeng DHuang YTan G(2025)Sliver: A Scalable Slicing-Based Verification for Information Flow SecurityIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2024.340365322:1(457-473)Online publication date: Jan-2025
https://doi.org/10.1109/TDSC.2024.3403653
Soares LCanesche MPereira F(2023)Side-channel Elimination via Partial Control-flow LinearizationACM Transactions on Programming Languages and Systems10.1145/359473645:2(1-43)Online publication date: 26-Jun-2023
https://dl.acm.org/doi/10.1145/3594736
Daniel LBardin SRezk T(2023)Binsec/Rel: Symbolic Binary Analyzer for Security with Applications to Constant-Time and Secret-ErasureACM Transactions on Privacy and Security10.1145/356303726:2(1-42)Online publication date: 14-Apr-2023
https://dl.acm.org/doi/10.1145/3563037
Guanciale RBaumann CBuiras PDam MNemati H(2022)A Case Study in Information Flow Refinement for Low Level SystemsThe Logic of Software. A Tasting Menu of Formal Methods10.1007/978-3-031-08166-8_4(54-79)Online publication date: 4-Jul-2022
https://doi.org/10.1007/978-3-031-08166-8_4
Tsoupidi RBalliu MBaudry B(2021)Vivienne: Relational Verification of Cryptographic Implementations in WebAssembly2021 IEEE Secure Development Conference (SecDev)10.1109/SecDev51306.2021.00029(94-102)Online publication date: Oct-2021
https://doi.org/10.1109/SecDev51306.2021.00029
Geraldo ESantos JSeco J(2021)Hybrid Information Flow Control for Low-Level CodeSoftware Engineering and Formal Methods10.1007/978-3-030-92124-8_9(141-159)Online publication date: 3-Dec-2021
https://doi.org/10.1007/978-3-030-92124-8_9
Guanciale RBalliu MDam MLigatti JOu XKatz JVigna G(2020)InSpectre: Breaking and Fixing Microarchitectural Vulnerabilities by Formal AnalysisProceedings of the 2020 ACM SIGSAC Conference on Computer and Communications Security10.1145/3372297.3417246(1853-1869)Online publication date: 30-Oct-2020
https://dl.acm.org/doi/10.1145/3372297.3417246
Daniel LBardin SRezk T(2020)Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level2020 IEEE Symposium on Security and Privacy (SP)10.1109/SP40000.2020.00074(1021-1038)Online publication date: May-2020
https://doi.org/10.1109/SP40000.2020.00074
Nemati HBuiras PLindner AGuanciale RJacobs S(2020)Validation of Abstract Side-Channel Models for Computer ArchitecturesComputer Aided Verification10.1007/978-3-030-53288-8_12(225-248)Online publication date: 14-Jul-2020
https://doi.org/10.1007/978-3-030-53288-8_12
Alrabaee SDebbabi MShirani PWang LYoussef ARahimian ANouh LMouheb DHuang HHanna AAlrabaee SDebbabi MShirani PWang LYoussef ARahimian ANouh LMouheb DHuang HHanna A(2020)IntroductionBinary Code Fingerprinting for Cybersecurity10.1007/978-3-030-34238-8_1(1-6)Online publication date: 1-Mar-2020
https://doi.org/10.1007/978-3-030-34238-8_1
Show More Cited By

View Options

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

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Figures

Tables

Media

View Table of Conten