short-paper

Short Paper: Towards Information Flow Reasoning about Real-World C Code

Authors:

Samuel Gruetter,

Toby MurrayAuthors Info & Claims

PLAS '17: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security

Pages 43 - 48

https://doi.org/10.1145/3139337.3139345

Published: 30 October 2017 Publication History

Abstract

Strangely, despite much recent success proving information flow control (IFC) security for C programs, little work has investigated how to prove IFC security directly against C code, as opposed to over an abstract specification. We consider what a suitable IFC logic for C might look like, and propose a suitable continuation-passing style IFC security definition for C code. We discuss our ongoing work implementing these ideas in the context of an existing full-featured, sound program verification framework for C, the Verified Software Toolchain, supported by the verified C complier CompCert.

References

[1]

Andrew W. Appel. 2015. Verification of a Cryptographic Primitive: SHA-256. ACM Transactions on Programming Languages and Systems 37, 2 (2015), 1--31.

Digital Library

[2]

Andrew W. Appel and Sandrine Blazy. 2007. Separation Logic for Small-Step Cminor. In Theorem Proving in Higher Order Logics. Springer, 5--21.

[3]

Andrew W. Appel, Robert Dockins, Aquinas Hobor, Lennart Beringer, Josiah Dodds, Gordon Stewart, Sandrine Blazy, and Xavier Leroy. 2014. Program Logics for Certified Compilers. Cambridge University Press, New York, NY, USA.

[4]

Andrew W. Appel and others. 2017. The Verified Software Toolchain. https://github.com/PrincetonUniversity/VST. (2017).

[5]

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

Digital Library

[6]

Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu, and Franco Raimondi. 2016. CoSMed: A Confidentiality-Verified Social Media Platform. In International Conference on Interactive Theorem Proving. Springer, 87--106.

[7]

Mark Beaumont, Jim McCarthy, and Toby Murray. 2016. The Cross Domain Desktop Compositor: Using Hardware-Based Video Compositing for a MultiLevel Secure User Interface. ACM Press, 533--545.

[8]

Lennart Beringer. 2011. Relational Decomposition. In International Conference on Interactive Theorem Proving. Springer, 39--54.

[9]

Lennart Beringer, Adam Petcher, Katherine Q. Ye, and Andrew W. Appel. 2015. Verified Correctness and Security of OpenSSL HMAC. In USENIX Security Symposium. 207--221.

[10]

Daniel J. Bernstein, Tanja Lange, and Peter Schwabe. NaCl: Networking and Cryptography library. Available at: http://nacl.cr.yp.to/. (????).

[11]

Daniel J. Bernstein, Tanja Lange, and Peter Schwabe. 2012. The Security Impact of a New Cryptographic Library. Santiago, CL, 159--176.

Digital Library

[12]

Sandrine Blazy, David Pichardie, and Alix Trieu. 2017. Verifying Constant-Time Implementations by Abstract Interpretation. In ESORICS. 260--277.

[13]

David Cock, Gerwin Klein, and Thomas Sewell. 2008. Secure Microkernels, State Monads and Scalable Refinement. In Proceedings of the 21st International Conference on Theorem Proving in Higher Order Logics (Lecture Notes in Computer Science), Vol. 5170. 167--182. https://doi.org/10.1007/978-3-540-71067-7_16

[14]

David Costanzo. 2016. Formal End-to-End Verification of Information-Flow Security for Complex Systems. Ph.D. Dissertation. Yale University. http://www.cs.yale.edu/homes/dsc5/thesis.pdf.

[15]

David Costanzo and Zhong Shao. 2014. A Separation Logic for Enforcing Declarative Information Flow Control Policies. In International Conference on Principles of Security and Trust. Springer, 179--198.

[16]

Florian Dewald, Heiko Mantel, and Alexandra Weber. 2017. AVR Processors as a Platform for Language-Based Security. In ESORICS.

[17]

Duncan A. Grove, Toby Murray, Chris A. Owen, Chris J. North, J. A. Jones, Mark R. Beaumont, and Bradley D. Hopkins. 2007. An overview of the Annex system. In Annual Computer Security Applications Conference (ACSAC). 341--352.

[18]

Samuel Gruetter. 2017. Improving the Coq proof automation tactics of the Verified Software Toolchain, based on a case study on verifying a C implementation of the AES encryption algorithm. Master's thesis. École Polytechnique Fédérale de Lausanne (EPFL), Switzerland.

[19]

Samuel Gruetter and Toby Murray. 2017. VST-Flow: Fine-Grained LowLevel Reasoning about Real-World C Code. arXiv:1709.05243 [cs] (Sept. 2017). arXiv:1709.05243

[20]

Ronghui Gu, Zhong Shao, Hao Chen, Xiongnan (Newman) Wu, Jieung Kim, Vilhelm Sjöberg, and David Costanzo. 2016. CertiKOS: An Extensible Architecture for Building Certified Concurrent OS Kernels. In OSDI.

[21]

C. A. R. Hoare. 1969. An Axiomatic Basis for Computer Programming. Commun. ACM 12, 10 (Oct. 1969), 576--580.

Digital Library

[22]

Sudeep Kanav, Peter Lammich, and Andrei Popescu. 2014. A conference management system with verified document confidentiality. In International Conference on Computer Aided Verification. Springer, 167--183.

Digital Library

[23]

Gerwin Klein, June Andronick, Kevin Elphinstone, Toby Murray, Thomas Sewell, Rafal Kolanski, and Gernot Heiser. 2014. Comprehensive Formal Verification of an OS Microkernel. ACM Transactions on Computer Systems 32, 1 (Feb. 2014), 2:1--2:70. https://doi.org/10.1145/2560537

Digital Library

[24]

Xavier Leroy. 2009. Formal verification of a realistic compiler. Commun. ACM 52, 7 (2009), 107--115. https://doi.org/10.1145/1538788.1538814

Digital Library

[25]

Luísa Lourenço and Luís Caires. 2015. Dependent Information Flow Types. In ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Mumbai, India, 317--328.

Digital Library

[26]

Donald A. MacKenzie. 2004. Mechanizing proof: computing, risk, and trust. MIT Press.

[27]

Toby Murray. 2015. Short Paper: On High-Assurance Information-Flow-Secure Programming Languages. In 10th ACM Workshop on Programming Languages and Analysis for Security (PLAS). 43--48.

Digital Library

[28]

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, Timothy Bourke, Sean Seefried, Corey Lewis, Xin Gao, and Gerwin Klein. 2013. seL4: from General Purpose to a Proof of Information Flow Enforcement. In IEEE Symposium on Security and Privacy. San Francisco, CA, 415--429. https://doi.org/10.1109/SP.2013.35

Digital Library

[29]

Toby Murray, Daniel Matichuk, Matthew Brassil, Peter Gammie, and Gerwin Klein. 2012. Noninterference for Operating System Kernels. In International Conference on Certified Programs and Proofs. Springer, Kyoto, Japan, 126--142.

Digital Library

[30]

Toby Murray, Andrei Sabelfeld, and Lujo Bauer. 2017. Guest editorial: Special issue on verified information flow security. Journal of Computer Security (2017). https://doi.org/10.3233/JCS-15801 To appear.

[31]

Peter W. O'Hearn. 2004. Concurrency, and Local Reasoning (LNCS), Vol. 3170.

[32]

John C. Reynolds. 2002. Separation logic: A logic for shared mutable data structures. In LICS. IEEE, 55--74.

[33]

Norbert Schirmer. 2006. Verification of Sequential Imperative Programs in Isabelle-HOL. Ph.D. Dissertation. Technical University Munich.

[34]

Thomas Sewell, Magnus Myreen, and Gerwin Klein. 2013. Translation Validation for a Verified OS Kernel. In ACM SIGPLAN Conference on Programming Language Design and Implementation. ACM, Seattle, Washington, USA, 471--481.

Digital Library

[35]

Harvey Tuch, Gerwin Klein, and Michael Norrish. 2007. Types, Bytes, and Separation Logic. In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. ACM, 97--108.

Digital Library

[36]

Simon Winwood, Gerwin Klein, Thomas Sewell, June Andronick, David Cock, and Michael Norrish. 2009. Mind the Gap: A Verification Framework for Low-Level C. In 22nd TPHOLs (LNCS), Stefan Berghofer, Tobias Nipkow, Christian Urban, and Makarius Wenzel (Eds.), Vol. 5674. Springer, Munich, Germany, 500--515.

[37]

Lantian Zheng and Andrew C. Myers. 2007. Dynamic security labels and Static Information Flow Control. International Journal of Information Security 6, 2-3 (March 2007).

Digital Library

Cited By

Naz HNijhawan RAhuja N(2022)An automated unsupervised deep learning–based approach for diabetic retinopathy detectionMedical & Biological Engineering & Computing10.1007/s11517-022-02688-960:12(3635-3654)Online publication date: 24-Oct-2022
https://doi.org/10.1007/s11517-022-02688-9
Ernst GMurray T(2019)SecCSL: Security Concurrent Separation LogicComputer Aided Verification10.1007/978-3-030-25543-5_13(208-230)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_13

Index Terms

Short Paper: Towards Information Flow Reasoning about Real-World C Code
1. Security and privacy
  1. Formal methods and theory of security
    1. Logic and verification
2. Theory of computation
  1. Logic
    1. Separation logic

Recommendations

A Certifying Compiler for Clike Subset of C Language
TASE '10: Proceedings of the 2010 4th IEEE International Symposium on Theoretical Aspects of Software Engineering

Proof-carrying code (PCC) is a technique that allows code consumers to check whether the code is safe to execute or not through a formal safety proof provided by the code producer. And a certifying compiler makes PCC practical by compiling annotated ...
Testing Dafny (experience paper)
ISSTA 2022: Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis

Verification toolchains are widely used to prove the correctness of critical software systems. To build confidence in their results, it is important to develop testing frameworks that help detect bugs in these toolchains. Inspired by the success of ...
Assume but Verify: Deductive Verification of Leaked Information in Concurrent Applications
CCS '23: Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security

We consider the problem of specifying and proving the security of non-trivial, concurrent programs that intentionally leak information. We present a method that decomposes the problem into (a) proving that the program only leaks information it has ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM Conferences

PLAS '17: Proceedings of the 2017 Workshop on Programming Languages and Analysis for Security

October 2017

128 pages

ISBN:9781450350990

DOI:10.1145/3139337

Program Chairs:
Nataliia Bielova
INRIA, France
,
Marco Gaboardi
University at Buffalo, SUNY, USA

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 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: 30 October 2017

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Author Tags

Qualifiers

Short-paper

Conference

CCS '17

Sponsor:

SIGSAC

CCS '17: 2017 ACM SIGSAC Conference on Computer and Communications Security

October 30, 2017

Texas, Dallas, USA

Acceptance Rates

PLAS '17 Paper Acceptance Rate 8 of 10 submissions, 80%;

Overall Acceptance Rate 43 of 77 submissions, 56%

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

2
Total Citations
View Citations
80
Total Downloads

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

Reflects downloads up to 18 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Naz HNijhawan RAhuja N(2022)An automated unsupervised deep learning–based approach for diabetic retinopathy detectionMedical & Biological Engineering & Computing10.1007/s11517-022-02688-960:12(3635-3654)Online publication date: 24-Oct-2022
https://doi.org/10.1007/s11517-022-02688-9
Ernst GMurray T(2019)SecCSL: Security Concurrent Separation LogicComputer Aided Verification10.1007/978-3-030-25543-5_13(208-230)Online publication date: 12-Jul-2019
https://doi.org/10.1007/978-3-030-25543-5_13

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.

Media

Figures

Other

Tables

View Table of Contents