skip to main content
10.1145/2676726.2676972acmconferencesArticle/Chapter ViewAbstractPublication PagespoplConference Proceedingsconference-collections
research-article

Sound Modular Verification of C Code Executing in an Unverified Context

Published: 14 January 2015 Publication History

Abstract

Over the past decade, great progress has been made in the static modular verification of C code by means of separation logic-based program logics. However, the runtime guarantees offered by such verification are relatively limited when the verified modules are part of a whole program that also contains unverified modules. In particular, a memory safety error in an unverified module can corrupt the runtime state, leading to assertion failures or invalid memory accesses in the verified modules. This paper develops runtime checks to be inserted at the boundary between the verified and the unverified part of a program, to guarantee that no assertion failures or invalid memory accesses can occur at runtime in any verified module. One of the key challenges is enforcing the separation logic frame rule, which we achieve by checking the integrity of the footprint of the verified part of the program on each control flow transition from the unverified to the verified part. This in turn requires the presence of some support for module-private memory at runtime. We formalize our approach and prove soundness. We implement the necessary runtime checks by means of a program transformation that translates C code with separation logic annotations into plain C, and that relies on a protected module architecture for providing module-private memory and restricted module entry points. Benchmarks show the performance impact of this transformation depends on the choice of boundary between the verified and unverified parts of the program, but is below 4% for real-world applications.

Supplementary Material

MPG File (p581-sidebyside.mpg)

References

[1]
M. Abadi. Protection in programming-language translations. In Proceedings of the 25th International Colloquium on Automata, Languages and Programming, ICALP '98, pages 868--883, London, UK, UK, 1998. Springer-Verlag. ISBN 3-540-64781-3.
[2]
P. Agten, R. Strackx, B. Jacobs, and F. Piessens. Secure compilation to modern processors. In Proceedings of the 2012 IEEE 25th Computer Security Foundations Symposium, CSF '12, pages 171--185, Washington, DC, USA, 2012. IEEE Computer Society. ISBN 978-0--7695--4718--3. URL http://dx.doi.org/10.1109/CSF.2012.12.
[3]
P. Agten, B. Bart Jacobs, and F. Piessens. Sound modular verification of C code executing in an unverified context: extended version. Technical Report CW 676, KU Leuven, 2014. URL http://www.cs.kuleuven.be/publicaties/rapporten/cw/CW676.abs.html.
[4]
T. M. Austin, S. E. Breach, and G. S. Sohi. Efficient detection of all pointer and array access errors. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation, PLDI '94, pages 290--301, New York, NY, USA, 1994. ACM. ISBN 0--89791--662-X. URL http://doi.acm.org/10.1145/178243.178446.
[5]
M. Barnett and W. Schulte. Runtime verification of .net contracts. J. Syst. Softw., 65(3):199--208, Mar. 2003. ISSN 0164-1212. URL http://dx.doi.org/10.1016/S0164--1212(02)00041--9.
[6]
J. Berdine, C. Calcagno, and P. W. O'Hearn. Smallfoot: Modular automatic assertion checking with separation logic. In Proceedings of the 4th International Conference on Formal Methods for Components and Objects, FMCO'05, pages 115--137, Berlin, Heidelberg, 2006. Springer-Verlag. ISBN 3-540-36749-7, 978-3-540-36749-9. URL http://dx.doi.org/10.1007/11804192_6.
[7]
L. Burdy, Y. Cheon, D. R. Cok, M. D. Ernst, J. R. Kiniry, G. T. Leavens, K. R. M. Leino, and E. Poll. An overview of jml tools and applications. Int. J. Softw. Tools Technol. Transf., 7(3):212--232, June 2005. ISSN 1433-2779. URL http://dx.doi.org/10.1007/s10009-004-0167-4.
[8]
C. Calcagno, D. Distefano, and V. Vafeiadis. Bi-abductive resource invariant synthesis. In Proceedings of the 7th Asian Symposium on Programming Languages and Systems, APLAS '09, pages 259--274, Berlin, Heidelberg, 2009. Springer-Verlag. ISBN 978--3--642--10671--2. URL http://dx.doi.org/10.1007/978-3-642-10672-9_19.
[9]
W.-N. Chin, C. David, H. H. Nguyen, and S. Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic. Sci. Comput. Program., 77(9):1006--1036, Aug. 2012. ISSN 0167-6423. URL http://dx.doi.org/10.1016/j.scico.2010.07.004.
[10]
E. Cohen, M. Dahlweid, M. Hillebrand, D. Leinenbach, M. Moskal, T. Santen, W. Schulte, and S. Tobies. Vcc: A practical system for verifying concurrent c. In Proceedings of the 22nd International Conference on Theorem Proving in Higher Order Logics, TPHOLs '09, pages 23--42, Berlin, Heidelberg, 2009. Springer-Verlag. ISBN 978-3-642-03358-2. URL http://dx.doi.org/10.1007/978-3-642-03359--9_2.
[11]
M. Dahlweid, M. Moskal, T. Santen, S. Tobies, and W. Schulte. Vcc: Contract-based modular verification of concurrent c. In 31st International Conference on Software Engineering, ICSE 2009, pages 429--430, May 2009.
[12]
C. Dimoulas, R. B. Findler, C. Flanagan, and M. Felleisen. Correct blame for contracts: No more scapegoating. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, pages 215--226, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0490-0. URL http://doi.acm.org/10.1145/1926385.1926410.
[13]
D. Distefano and M. J. Parkinson J. jstar: Towards practical verification for java. In Proceedings of the 23rd ACM SIGPLAN Conference on Object-oriented Programming Systems Languages and Applications, OOPSLA '08, pages 213--226, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-215-3. URL http://doi.acm.org/10.1145/1449764.1449782.
[14]
U. Erlingsson. Low-level software security: Attacks and defenses. In A. Aldini and R. Gorrieri, editors, Foundations of Security Analysis and Design IV, pages 92--134. Springer-Verlag, Berlin, Heidelberg, 2007. ISBN 3-540-74809-1, 978-3-540-74809-0. URL http://dl.acm.org/citation.cfm?id=1793914.1793919.
[15]
R. B. Findler and M. Felleisen. Contract soundness for object-oriented languages. In Proceedings of the 16th ACM SIGPLAN Conference on Object-oriented Programming, Systems, Languages, and Applications, OOPSLA '01, pages 1--15, New York, NY, USA, 2001. ACM. ISBN 1-58113-335-9. URL http://doi.acm.org/10.1145/504282.504283.
[16]
M. Flatt and PLT. Reference: Racket. Technical Report PLT-TR-2010--1, PLT Inc., 2010. http://racket-lang.org/tr1/.
[17]
C. Fournet, N. Swamy, J. Chen, P.-E. Dagand, P.-Y. Strub, and B. Livshits. Fully abstract compilation to javascript. In Proceedings of the 40th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '13, pages 371--384, New York, NY, USA, 2013. ACM. ISBN 978-1-4503-1832-7. URL http://doi.acm.org/10.1145/2429069.2429114.
[18]
M. Greenberg, B. C. Pierce, and S. Weirich. Contracts made manifest. In Proceedings of the 37th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '10, pages 353--364, New York, NY, USA, 2010. ACM. ISBN 978-1-60558-479-9. URL http://doi.acm.org/10.1145/1706299.1706341.
[19]
J. Guo, P. Karpman, I. Nikolic, L. Wang, and S. Wu. Analysis of blake2. Cryptology ePrint Archive, Report 2013/467, 2013. http://eprint.iacr.org/.
[20]
Intel Corporation. Intel software guard extensions, 2013. URL http://software.intel.com/en-us/intel-isa-extensions#pid-19539-1495.
[21]
B. Jacobs and F. Piessens. Expressive modular fine-grained concurrency specification. In Proceedings of the 38th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '11, pages 271--282, New York, NY, USA, 2011. ACM. ISBN 978-1-4503-0490-0. URL http://doi.acm.org/10.1145/1926385.1926417.
[22]
B. Jacobs, J. Smans, and F. Piessens. A quick tour of the verifast program verifier. In Proceedings of the 8th Asian Conference on Programming Languages and Systems, APLAS'10, 2010.
[23]
T. Jim, J. G. Morrisett, D. Grossman, M. W. Hicks, J. Cheney, and Y. Wang. Cyclone: A safe dialect of c. In Proceedings of the General Track of the Annual Conference on USENIX Annual Technical Conference, ATEC '02, pages 275--288, Berkeley, CA, USA, 2002. USENIX Association. ISBN 1-880446-00-6. URL http://dl.acm.org/citation.cfm?id=647057.713871.
[24]
G. Klein, K. Elphinstone, G. Heiser, J. Andronick, D. Cock, P. Derrin, D. Elkaduwe, K. Engelhardt, R. Kolanski, M. Norrish, T. Sewell, H. Tuch, and S. Winwood. sel4: Formal verification of an os kernel. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, SOSP '09, pages 207--220, New York, NY, USA, 2009. ACM. ISBN 978-1-60558-752-3. URL http://doi.acm.org/10.1145/1629575.1629596.
[25]
N. Kosmatov, G. Petiot, and J. Signoles. An optimized memory monitoring for runtime assertion checking of C programs. In Runtime Verification - 4th International Conference, RV 2013, Rennes, France, September 24--27, 2013. Proceedings, pages 167--182, 2013. URL http://dx.doi.org/10.1007/978-3-642-40787-1_10.
[26]
J. M. McCune, B. J. Parno, A. Perrig, M. K. Reiter, and H. Isozaki. Flicker: An execution infrastructure for tcb minimization. In Proceedings of the 3rd ACM SIGOPS/EuroSys European Conference on Computer Systems 2008, Eurosys '08, pages 315--328, New York, NY, USA, 2008. ACM. ISBN 978-1-60558-013-5. URL http://doi.acm.org/10.1145/1352592.1352625.
[27]
B. Meyer. Applying "design by contract". Computer, 25(10):40--51, Oct. 1992. ISSN 0018-9162. URL http://dx.doi.org/10.1109/2.161279.
[28]
G. C. Necula, S. McPeak, and W. Weimer. Ccured: Type-safe retrofitting of legacy code. In Proceedings of the 29th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL'02, pages 128--139, New York, NY, USA, 2002. ACM. ISBN 1-58113-450-9. URL http://doi.acm.org/10.1145/503272.503286.
[29]
H. H. Nguyen, V. Kuncak, and W.-N. Chin. Runtime checking for separation logic. In Proceedings of the 9th International Conference on Verification, Model Checking, and Abstract Interpretation, VM- CAI'08, pages 203--217, Berlin, Heidelberg, 2008. Springer-Verlag. ISBN 3-540-78162-5, 978-3-540-78162-2. URL http://dl.acm.org/citation.cfm?id=1787526.1787545.
[30]
J. Noorman, P. Agten, W. Daniels, R. Strackx, A. Van Herrewege, C. Huygens, B. Preneel, I. Verbauwhede, and F. Piessens. Sancus: Low-cost trustworthy extensible networked devices with a zero- software trusted computing base. In Proceedings of the 22nd USENIX Conference on Security, SEC'13, pages 479--494, Berkeley, CA, USA, 2013. USENIX Association. ISBN 978-1-931971-03-4. URL http://dl.acm.org/citation.cfm?id=2534766.2534808.
[31]
M. Patrignani, P. Agten, R. Strackx, B. Jacobs, D. Clarke, and F. Piessens. Secure compilation to protected module architectures. ACM Transactions on Programming Languages and Systems (TOPLAS), accepted for publication in ACM TOPLAS.
[32]
P. Philippaerts, J. T. Mühlberg, W. Penninckx, J. Smans, B. Jacobs, and F. Piessens. Software verification with VeriFast: Industrial case studies. Science of Computer Programming, 82(1):77--97, Mar. 2014. URL https://lirias.kuleuven.be/handle/123456789/388689.
[33]
J. C. Reynolds. Separation logic: A logic for shared mutable data structures. In Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, LICS '02, pages 55--74, Washington, DC, USA, 2002. IEEE Computer Society. ISBN 0-7695-1483-9. URL http://dl.acm.org/citation.cfm?id=645683.664578.
[34]
C. Schlesinger, K. Pattabiraman, N. Swamy, D. Walker, and B. Zorn. Modular protections against non-control data attacks. In Proceedings of the 2011 IEEE 24th Computer Security Foundations Symposium, CSF '11, pages 131--145, Washington, DC, USA, 2011. IEEE Computer Society. ISBN 978-0-7695-4365-9. URL http://dx.doi.org/10.1109/CSF.2011.16.
[35]
R. Strackx and F. Piessens. Fides: Selectively hardening software application components against kernel-level or process-level malware. In Proceedings of the 2012 ACM Conference on Computer and Communications Security, CCS '12, pages 2--13, New York, NY, USA, 2012. ACM. ISBN 978-1-4503-1651-4. URL http://doi.acm.org/10.1145/2382196.2382200.
[36]
N. Swamy, C. Fournet, A. Rastogi, K. Bhargavan, J. Chen, P.-Y. Strub, and G. Bierman. Gradual typing embedded securely in javascript. In Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '14, pages 425--437, New York, NY, USA, 2014. ACM. ISBN 978-1-4503-2544-8.
[37]
A. Vasudevan, S. Chaki, L. Jia, J. McCune, J. Newsome, and A. Datta. Design, implementation and verification of an extensible and modular hypervisor framework. In Proceedings of the 2013 IEEE Symposium on Security and Privacy, SP '13, pages 430--444, Washington, DC, USA, 2013. IEEE Computer Society. ISBN 978-0-7695-4977-4. URL http://dx.doi.org/10.1109/SP.2013.36.

Cited By

View all
  • (2025)Fulminate: Testing CN Separation-Logic Specifications in CProceedings of the ACM on Programming Languages10.1145/37048799:POPL(1260-1292)Online publication date: 9-Jan-2025
  • (2024)Gradual C0: Symbolic Execution for Gradual VerificationACM Transactions on Programming Languages and Systems10.1145/370480846:4(1-57)Online publication date: 5-Dec-2024
  • (2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM Conferences
POPL '15: Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
January 2015
716 pages
ISBN:9781450333009
DOI:10.1145/2676726
  • cover image ACM SIGPLAN Notices
    ACM SIGPLAN Notices  Volume 50, Issue 1
    POPL '15
    January 2015
    682 pages
    ISSN:0362-1340
    EISSN:1558-1160
    DOI:10.1145/2775051
    • Editor:
    • Andy Gill
    Issue’s Table of Contents
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

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 14 January 2015

Permissions

Request permissions for this article.

Check for updates

Author Tags

  1. runtime checking
  2. separation logic
  3. verification

Qualifiers

  • Research-article

Funding Sources

Conference

POPL '15
Sponsor:

Acceptance Rates

POPL '15 Paper Acceptance Rate 52 of 227 submissions, 23%;
Overall Acceptance Rate 860 of 4,328 submissions, 20%

Upcoming Conference

POPL '26

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)28
  • Downloads (Last 6 weeks)2
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)Fulminate: Testing CN Separation-Logic Specifications in CProceedings of the ACM on Programming Languages10.1145/37048799:POPL(1260-1292)Online publication date: 9-Jan-2025
  • (2024)Gradual C0: Symbolic Execution for Gradual VerificationACM Transactions on Programming Languages and Systems10.1145/370480846:4(1-57)Online publication date: 5-Dec-2024
  • (2024)Securing Verified IO Programs Against Unverified Code in F*Proceedings of the ACM on Programming Languages10.1145/36329168:POPL(2226-2259)Online publication date: 5-Jan-2024
  • (2023)Verification-Preserving Inlining in Automatic Separation Logic VerifiersProceedings of the ACM on Programming Languages10.1145/35860547:OOPSLA1(789-818)Online publication date: 6-Apr-2023
  • (2022)Proving full-system security properties under multiple attacker models on capability machines2022 IEEE 35th Computer Security Foundations Symposium (CSF)10.1109/CSF54842.2022.9919645(80-95)Online publication date: Aug-2022
  • (2021)Rich specifications for Ethereum smart contract verificationProceedings of the ACM on Programming Languages10.1145/34855235:OOPSLA(1-30)Online publication date: 15-Oct-2021
  • (2019)Linear capabilities for fully abstract compilation of separation-logic-verified codeProceedings of the ACM on Programming Languages10.1145/33416883:ICFP(1-29)Online publication date: 26-Jul-2019
  • (2018)When Good Components Go BadProceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security10.1145/3243734.3243745(1351-1368)Online publication date: 15-Oct-2018
  • (2017)Verifying Invariants of Lock-Free Data Structures with Rely-Guarantee and Refinement TypesACM Transactions on Programming Languages and Systems10.1145/306485039:3(1-54)Online publication date: 10-May-2017
  • (2017)Efficient Incrementalized Runtime Checking of Linear Measures on Lists2017 IEEE International Conference on Software Testing, Verification and Validation (ICST)10.1109/ICST.2017.35(310-320)Online publication date: Mar-2017
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media