Skip to main content
SpringerLink
Log in

Flexible Runtime Security Enforcement with Tagged C

  • Conference paper
  • First Online:
Runtime Verification (RV 2023)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 14245))

Included in the following conference series:

  • 322 Accesses

Abstract

We introduce Tagged C, a novel C variant with built-in tag-based reference monitoring that can be enforced by hardware mechanisms such as the PIPE (Processor Interlocks for Policy Enforcement) processor extension. Tagged C expresses security policies at the level of C source code. It is designed to express a variety of dynamic security policies, individually or in combination, and enforce them with compiler and hardware support. Tagged C supports multiple approaches to security and varying levels of strictness. We demonstrate this range by providing examples of memory safety, compartmentalization, and secure information flow policies. We also give a full formalized semantics and a reference interpreter for Tagged C.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 59.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 79.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Similar content being viewed by others

Notes

  1. 1.

    Variants of PIPE have been called PUMP [15] or SDMP [27] and marketed commercially under the names Dover CoreGuard and Draper Inherently Secure Processor.

  2. 2.

    Available at https://github.com/SNoAnd/Tagged-C.

  3. 3.

    For simplicity, we omit showing tag rules that play no interesting role in this example: and , which are triggered each time a variable is read and assigned, respectively, and , which is triggered by the call itself.

  4. 4.

    It inherits the limitations of CompCert C, primarily that setjump and longjump may not work, and variable-length arrays are not supported.

  5. 5.

    Not to be confused with the control-flow graph join points discussed in Sect. 4.3.

References

  1. Anderson, J.P.: Computer security technology planning study. Technical report ESD-TR-73-51, U.S. Air Force Electronic Systems Division (1972). http://csrc.nist.gov/publications/history/ande72.pdf

  2. Armv8.5-a memory tagging extension white paper. https://developer.arm.com/-/media/Arm%20Developer%20Community/PDF/Arm_Memory_Tagging_Extension_Whitepaper.pdf

  3. Austin, T.H., Flanagan, C.: Multiple facets for dynamic information flow. In: Proceedings of the 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2012, pp. 165–178. Association for Computing Machinery (2012). https://doi.org/10.1145/2103656.2103677

  4. Azevedo de Amorim, A., et al.: A verified information-flow architecture. J. Comput. Secur. 24(6), 689–734 (2016). https://doi.org/10.3233/JCS-15784

    Article  Google Scholar 

  5. Azevedo de Amorim, A., et al.: Micro-policies: formally verified, tag-based security monitors. In: 2015 IEEE Symposium on Security and Privacy, pp. 813–830 (2015). https://doi.org/10.1109/SP.2015.55

  6. Ball, T., Rajamani, S.: SLIC: a specification language for interface checking (of C). Technical report MSR-TR-2001-21 (2002). https://www.microsoft.com/en-us/research/publication/slic-a-specification-language-for-interface-checking-of-c/

  7. Bessey, A., et al.: A few billion lines of code later: using static analysis to find bugs in the real world. Commun. ACM 53(2), 66–75 (2010). https://doi.org/10.1145/1646353.1646374

    Article  Google Scholar 

  8. Cassel, D., Huang, Y., Jia, L.: Uncovering information flow policy violations in C programs (extended abstract). In: Sako, K., Schneider, S., Ryan, P.Y.A. (eds.) ESORICS 2019. LNCS, vol. 11736, pp. 26–46. Springer, Cham (2019). https://doi.org/10.1007/978-3-030-29962-0_2

    Chapter  Google Scholar 

  9. Chabot, M., Mazet, K., Pierre, L.: Automatic and configurable instrumentation of C programs with temporal assertion checkers. In: 2015 ACM/IEEE International Conference on Formal Methods and Models for Codesign (MEMOCODE), pp. 208–217 (2015). https://doi.org/10.1109/MEMCOD.2015.7340488

  10. Chhak, C., Tolmach, A., Anderson, S.: Towards formally verified compilation of tag-based policy enforcement. In: Proceedings of the 10th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 137–151 (2021). https://doi.org/10.1145/3437992.3439929

  11. Clause, J., Doudalis, I., Orso, A., Prvulovic, M.: Effective memory protection using dynamic tainting. In: Proceedings of the 22nd IEEE/ACM International Conference on Automated Software Engineering, pp. 284–292 (2007). https://doi.org/10.1145/1321631.1321673

  12. Coq Team: The Coq proof assistant. https://coq.inria.fr

  13. Denning, D.E.: A lattice model of secure information flow. Commun. ACM 19(5), 236–243 (1976). https://doi.org/10.1145/360051.360056

    Article  MathSciNet  MATH  Google Scholar 

  14. Denning, D.E., Denning, P.J.: Certification of programs for secure information flow. Commun. ACM 20(7), 504–513 (1977). https://doi.org/10.1145/359636.359712

    Article  MATH  Google Scholar 

  15. Dhawan, U., et al.: Architectural support for software-defined metadata processing. In: Proceedings of the Twentieth International Conference on Architectural Support for Programming Languages and Operating Systems, pp. 487–502 (2015). https://doi.org/10.1145/2694344.2694383

  16. Engler, D.R., Chelf, B., Chou, A., Hallem, S.: Checking system rules using system-specific, programmer-written compiler extensions. In: OSDI, pp. 1–16 (2000)

    Google Scholar 

  17. Gollapudi, R., et al.: Control flow and pointer integrity enforcement in a secure tagged architecture. In: 2023 IEEE Symposium on Security and Privacy (SP), pp. 2974–2989 (2023). https://doi.ieeecomputersociety.org/10.1109/SP46215.2023.00102

  18. Havelund, K.: Runtime verification of C programs. In: Suzuki, K., Higashino, T., Ulrich, A., Hasegawa, T. (eds.) FATES/TestCom -2008. LNCS, vol. 5047, pp. 7–22. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-68524-1_3

    Chapter  Google Scholar 

  19. Kiczales, G., et al.: Aspect-oriented programming. In: Akşit, M., Matsuoka, S. (eds.) ECOOP 1997. LNCS, vol. 1241, pp. 220–242. Springer, Heidelberg (1997). https://doi.org/10.1007/BFb0053381

    Chapter  Google Scholar 

  20. Lampson, B.W.: Protection. SIGOPS Oper. Syst. Rev. 8(1), 18–24 (1974). https://doi.org/10.1145/775265.775268

    Article  MATH  Google Scholar 

  21. Leroy, X.: Compcert 3.10. https://github.com/AbsInt/CompCert/releases/tag/v3.10

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

    Article  Google Scholar 

  23. Leroy, X.: A formally verified compiler back-end. J. Autom. Reason. 43(4), 363–446 (2009). https://doi.org/10.1007/s10817-009-9155-4

    Article  MathSciNet  MATH  Google Scholar 

  24. Memarian, K., et al.: Exploring C semantics and pointer provenance. Proc. ACM Program. Lang. 3(POPL), 1–32 (2019). https://doi.org/10.1145/3290380

  25. Memarian, K., et al.: Into the depths of C: elaborating the de facto standards. SIGPLAN Not. 51(6), 1–15 (2016). https://doi.org/10.1145/2980983.2908081

    Article  Google Scholar 

  26. Michael, A.E., et al.: MSWasm: soundly enforcing memory-safe execution of unsafe code. Proc. ACM Program. Lang. 7(POPL), 425–454 (2023). https://doi.org/10.1145/3571208

  27. Roessler, N., DeHon, A.: Protecting the stack with metadata policies and tagged hardware. In: Proceedings of the 2018 IEEE Symposium on Security and Privacy, SP 2018, pp. 478–495 (2018). https://doi.org/10.1109/SP.2018.00066

  28. Russo, A., Sabelfeld, A.: Dynamic vs. static flow-sensitive security analysis. In: 2010 23rd IEEE Computer Security Foundations Symposium, pp. 186–199 (2010). https://doi.org/10.1109/CSF.2010.20

  29. Tsampas, S., El-Korashy, A., Patrignani, M., Devriese, D., Garg, D., Piessens, F.: Towards automatic compartmentalization of C programs on capability machines (2017). https://api.semanticscholar.org/CorpusID:32838507

  30. Filardo, N.W., et al.: Cornucopia: temporal safety for CHERI heaps. In: 2020 IEEE Symposium on Security and Privacy (SP), pp. 608–625 (2020). https://doi.org/10.1109/SP40000.2020.00098

Download references

Acknowledgements

We thank the reviewers for their valuable feedback, and Roberto Blanco for his advice during the writing process. This work was supported by the National Science Foundation under Grant No. 2048499, Specifying and Verifying Secure Compilation of C Code to Tagged Hardware.

Author information

Authors and Affiliations

  1. Portland State University, Portland, OR, USA

    Sean Anderson, Allison Naaktgeboren & Andrew Tolmach

Authors
  1. Sean Anderson
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Allison Naaktgeboren
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Andrew Tolmach
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Sean Anderson .

Editor information

Editors and Affiliations

  1. Dept. of Informatics, Aristotle Univ. of Thessaloniki, Thessaloniki, Greece

    Panagiotis Katsaros

  2. University of Trieste, Trieste, Italy

    Laura Nenzi

Rights and permissions

Reprints and permissions

Copyright information

© 2023 The Author(s), under exclusive license to Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Anderson, S., Naaktgeboren, A., Tolmach, A. (2023). Flexible Runtime Security Enforcement with Tagged C. In: Katsaros, P., Nenzi, L. (eds) Runtime Verification. RV 2023. Lecture Notes in Computer Science, vol 14245. Springer, Cham. https://doi.org/10.1007/978-3-031-44267-4_12

Download citation

  • DOI: https://doi.org/10.1007/978-3-031-44267-4_12

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-031-44266-7

  • Online ISBN: 978-3-031-44267-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation