article

Public Access

End-to-end verification of information-flow security for C and assembly programs

Authors:

David Costanzo,

Ronghui GuAuthors Info & Claims

ACM SIGPLAN Notices, Volume 51, Issue 6

Pages 648 - 664

https://doi.org/10.1145/2980983.2908100

Published: 02 June 2016 Publication History

Abstract

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly; we verify all of the code, regardless of language.

References

[1]

S. Blazy and X. Leroy. Mechanized semantics for the Clight subset of the C language. J. Automated Reasoning, 43(3): 263–288, 2009.

[2]

S. Chiricescu, A. DeHon, D. Demange, S. Iyer, A. Kliger, G. Morrisett, B. C. Pierce, H. Reubenstein, J. M. Smith, G. T. Sullivan, A. Thomas, J. Tov, C. M. White, and D. Wittenberg. Safe: A clean-slate architecture for secure systems. In Proceedings of the IEEE International Conference on Technologies for Homeland Security, Nov. 2013.

[3]

D. Costanzo and Z. Shao. A separation logic for enforcing declarative information flow control policies. In Proc. 3rd International Conference on Principles of Security and Trust (POST), pages 179–198, 2014.

[4]

D. Costanzo, Z. Shao, and R. Gu. End-to-end verification of information-flow security for C and assembly programs (extended version). Technical Report YALEU/DCS/TR-1522, Dept. of Computer Science, Yale University, April 2016.

[5]

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 2013 ACM SIGSAC Conference on Computer and Communications Security (CCS), pages 223–234, 2013.

Digital Library

[6]

L. M. de Moura and N. Bjørner. Z3: an efficient SMT solver. In Tools and Algorithms for the Construction and Analysis of Systems, 14th International Conference (TACAS), Budapest, Hungary. Proceedings, pages 337–340, 2008.

Digital Library

[7]

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

[8]

J. A. Goguen and J. Meseguer. Unwinding and inference control. In Proceedings of the 1984 IEEE Symposium on Security and Privacy, Oakland, California, USA, April 29 - May 2, 1984, pages 75–87, 1984.

[9]

R. Gu, J. Koenig, T. Ramananandro, Z. Shao, X. N. Wu, S. Weng, H. Zhang, and Y. Guo. Deep specifications and certified abstraction layers. In Proc. 42nd ACM SIGPLANSIGACT Symposium on Principles of Programming Languages (POPL), Mumbai, India, pages 595–608, 2015.

Digital Library

[10]

C. Hawblitzel, J. Howell, J. R. Lorch, A. Narayan, B. Parno, D. Zhang, and B. Zill. Ironclad apps: End-to-end security via automated full-system verification. In 11th USENIX Symposium on Operating Systems Design and Implementation (OSDI), Broomfield, CO, USA, pages 165–181, 2014.

Digital Library

[11]

J. Jürjens. Secrecy-preserving refinement. In FME 2001: Formal Methods for Increasing Software Productivity, International Symposium of Formal Methods Europe, Berlin, Germany, March 12-16, 2001, Proceedings, pages 135–152, 2001.

Digital Library

[12]

G. Klein, J. Andronick, K. Elphinstone, T. Murray, T. Sewell, R. Kolanski, and G. Heiser. Comprehensive formal verification of an OS microkernel. ACM Transactions on Computer Systems, 32(1), Feb. 2014.

Digital Library

[13]

K. R. M. Leino. Dafny: An automatic program verifier for functional correctness. In Logic for Programming, Artificial Intelligence, and Reasoning (LPAR) - 16th International Conference, Dakar, Senegal, pages 348–370, 2010.

Digital Library

[14]

X. Leroy. The CompCert verified compiler. http:// compcert.inria.fr/, 2005–2014.

[15]

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

Digital Library

[16]

P. Li and S. Zdancewic. Downgrading policies and relaxed noninterference. In Proc. 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Long Beach, California, USA, pages 158–170, 2005.

Digital Library

[17]

C. Morgan. The shadow knows: Refinement and security in sequential programs. Sci. Comput. Program., 74(8):629–653, 2009.

Digital Library

[18]

C. Morgan. Compositional noninterference from first principles. Formal Asp. Comput., 24(1):3–26, 2012.

[19]

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, and G. Klein. Noninterference for operating system kernels. In Certified Programs and Proofs (CPP) - Second International Conference, Kyoto, Japan, Proceedings, pages 126–142, 2012.

Digital Library

[20]

T. C. Murray, D. Matichuk, M. Brassil, P. Gammie, T. Bourke, S. Seefried, C. Lewis, X. Gao, and G. Klein. sel4: From general purpose to a proof of information flow enforcement. In IEEE Symposium on Security and Privacy, pages 415–429, 2013.

Digital Library

[21]

A. C. Myers and B. Liskov. A decentralized model for information flow control. In Proc. 1997 ACM Symposium on Operating System Principles (SOSP), pages 129–142, 1997.

Digital Library

[22]

A. Nanevski, A. Banerjee, and D. Garg. Verification of information flow and access control policies with dependent types. In IEEE Symposium on Security and Privacy, pages 165–179, 2011.

Digital Library

[23]

A. Sabelfeld and A. C. Myers. A model for delimited information release. In Software Security - Theories and Systems, Second Mext-NSF-JSPS International Symposium (ISSS), Tokyo, Japan, pages 174–191, 2003.

[24]

A. Sabelfeld and A. C. Myers. Language-based informationflow security. IEEE Journal on Selected Areas in Communications, 21(1):5–19, 2003.

Digital Library

[25]

A. Sabelfeld and D. Sands. A Per model of secure information flow in sequential programs. In Programming Languages and Systems, 8th European Symposium on Programming (ESOP), Amsterdam, The Netherlands, Proceedings, pages 40–58, 1999.

Digital Library

[26]

T. Sewell, S. Winwood, P. Gammie, T. C. Murray, J. Andronick, and G. Klein. seL4 enforces integrity. In Interactive Theorem Proving (ITP) - Second International Conference, Berg en Dal, The Netherlands, Proceedings, pages 325–340, 2011.

Digital Library

[27]

The Coq development team. The Coq proof assistant. http: //coq.inria.fr, 1999 – 2015.

Cited By

Gaurav AArya V(2024)Foundations of CybersecurityMetaverse Security Paradigms10.4018/979-8-3693-3824-7.ch004(77-107)Online publication date: 21-Aug-2024
https://doi.org/10.4018/979-8-3693-3824-7.ch004
Miao XChang RZhao JZhao YCao SWei TJiang LRen K(2023)CVTEE: A Compatible Verified TEE Architecture With Enhanced SecurityIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2021.313357620:1(377-391)Online publication date: 1-Jan-2023
https://doi.org/10.1109/TDSC.2021.3133576
Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Show More Cited By

Index Terms

Recommendations

End-to-end verification of information-flow security for C and assembly programs
PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end ...
Toward compositional verification of interruptible OS kernels and device drivers
PLDI '16

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified ...
Toward Compositional Verification of Interruptible OS Kernels and Device Drivers

An operating system (OS) kernel forms the lowest level of any system software stack. The correctness of the OS kernel is the basis for the correctness of the entire system. Recent efforts have demonstrated the feasibility of building formally verified ...

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 51, Issue 6

PLDI '16

June 2016

726 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2980983

Editor:
Andy Gill
University of Kansas, Lawrence, KS

Issue’s Table of Contents

PLDI '16: Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation
June 2016
726 pages
ISBN:9781450342612
DOI:10.1145/2908080
General Chair:
Chandra Krintz
University of California at Santa Barbara, USA
,
Program Chair:
Emery Berger
University of Massachusetts at Amherst, USA

Copyright © 2016 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].

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 02 June 2016

Published in SIGPLAN Volume 51, Issue 6

Check for updates

Author Tags

Qualifiers

Article

Funding Sources

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

51
Total Citations
View Citations
1,482
Total Downloads

Downloads (Last 12 months)232
Downloads (Last 6 weeks)49

Reflects downloads up to 01 Mar 2025

Other Metrics

View Author Metrics

Citations

Cited By

Gaurav AArya V(2024)Foundations of CybersecurityMetaverse Security Paradigms10.4018/979-8-3693-3824-7.ch004(77-107)Online publication date: 21-Aug-2024
https://doi.org/10.4018/979-8-3693-3824-7.ch004
Miao XChang RZhao JZhao YCao SWei TJiang LRen K(2023)CVTEE: A Compatible Verified TEE Architecture With Enhanced SecurityIEEE Transactions on Dependable and Secure Computing10.1109/TDSC.2021.313357620:1(377-391)Online publication date: 1-Jan-2023
https://doi.org/10.1109/TDSC.2021.3133576
Derakhshan FZhang ZVasudevan AJia L(2023)Towards End-to-End Verified TEEs via Verified Interface Conformance and Certified Compilers2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00021(324-339)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00021
Sison RBuckley SMurray TKlein GHeiser G(2023)Formalising the Prevention of Microarchitectural Timing Channels by Operating SystemsFormal Methods10.1007/978-3-031-27481-7_8(103-121)Online publication date: 3-Mar-2023
https://doi.org/10.1007/978-3-031-27481-7_8
Bhushan RYadav D(2022)A Survey on Formal Verification of Separation KernelsRecent Advances in Computer Science and Communications10.2174/266625581366620120715423015:6Online publication date: Jul-2022
https://doi.org/10.2174/2666255813666201207154230
Oliveira Vale AMelliès PShao ZKoenig JStefanesco L(2022)Layered and object-based game semanticsProceedings of the ACM on Programming Languages10.1145/34987036:POPL(1-32)Online publication date: 12-Jan-2022
https://dl.acm.org/doi/10.1145/3498703
Hu SHua BXia LWang Y(2022)CRUST: Towards a Unified Cross-Language Program Analysis Framework for Rust2022 IEEE 22nd International Conference on Software Quality, Reliability and Security (QRS)10.1109/QRS57517.2022.00101(970-981)Online publication date: Dec-2022
https://doi.org/10.1109/QRS57517.2022.00101
Taimoor Khan M(2022)Towards Practical and Formal Security Risk Analysis of IoT (Internet of Things) Applications2022 IEEE 27th International Conference on Emerging Technologies and Factory Automation (ETFA)10.1109/ETFA52439.2022.9921511(1-4)Online publication date: 6-Sep-2022
https://dl.acm.org/doi/10.1109/ETFA52439.2022.9921511
Patrignani MGarg D(2021)Robustly Safe Compilation, an Efficient Form of Secure CompilationACM Transactions on Programming Languages and Systems10.1145/343680943:1(1-41)Online publication date: 9-Feb-2021
https://dl.acm.org/doi/10.1145/3436809
Nelson LBornholt JKrishnamurthy ATorlak EWang X(2020)Noninterference specifications for secure systemsACM SIGOPS Operating Systems Review10.1145/3421473.342147854:1(31-39)Online publication date: 31-Aug-2020
https://dl.acm.org/doi/10.1145/3421473.3421478
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

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

Figures

Tables

Media

View Issue’s Table of Contents