Skip to main content
SpringerLink
Log in

Explicit Auditing

  • Conference paper
  • First Online:
Theoretical Aspects of Computing – ICTAC 2018 (ICTAC 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11187))

Included in the following conference series:

  • 505 Accesses

Abstract

The Calculus of Audited Units (CAU) is a typed lambda calculus resulting from a computational interpretation of Artemov’s Justification Logic under the Curry-Howard isomorphism; it extends the simply typed lambda calculus by providing audited types, inhabited by expressions carrying a trail of their past computation history. Unlike most other auditing techniques, CAU allows the inspection of trails at runtime as a first-class operation, with applications in security, debugging, and transparency of scientific computation.

An efficient implementation of CAU is challenging: not only do the sizes of trails grow rapidly, but they also need to be normalized after every beta reduction. In this paper, we study how to reduce terms more efficiently in an untyped variant of CAU by means of explicit substitutions and explicit auditing operations, finally deriving a call-by-value abstract machine.

An extended version of this paper can be found at https://arxiv.org/abs/1808.00486.

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 69.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 89.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

Notes

  1. 1.

    Although the right branch describes an unfaithful account of history, it is still a coherent one: we will explain this in more detail in the conclusions.

References

  1. Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991). https://doi.org/10.1017/s0956796800000186

    Article  MathSciNet  MATH  Google Scholar 

  2. Abadi, M., Fournet, C.: Access control based on execution history. In: Proceedings of Network and Distributed System Security Symposium, NDSS 2003, San Diego, CA. The Internet Society (2003) http://www.isoc.org/isoc/conferences/ndss/03/proceedings/papers/7.pdf

  3. Accattoli, B., Barenbaum, P., Mazza, D.: Distilling abstract machines. In: Proceedings of 19th ACM SIGPLAN Conference on Functional Programming, ICFP 2014, Gothenburg, September 2014, pp. 363–376. ACM Press, New York (2014). https://doi.org/10.1145/2628136.2628154

  4. Accattoli, B., Bonelli, E., Kesner, D., Lombardi, C.: A nonstandard standardization theorem. In: Proceedings of 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2014, San Diego, CA, January 2014, pp. 659–670. ACM Press, New York (2014). https://doi.org/10.1145/2535838.2535886

  5. Accattoli, B., Kesner, D.: The structural \(\lambda \)-calculus. In: Dawar, A., Veith, H. (eds.) CSL 2010. LNCS, vol. 6247, pp. 381–395. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-15205-4_30

    Chapter  Google Scholar 

  6. Amir-Mohammadian, S., Chong, S., Skalka, C.: Correct audit logging: theory and practice. In: Piessens, F., Viganò, L. (eds.) POST 2016. LNCS, vol. 9635, pp. 139–162. Springer, Heidelberg (2016). https://doi.org/10.1007/978-3-662-49635-0_8

    Chapter  Google Scholar 

  7. Artemov, S.: Justification logic. In: Hölldobler, S., Lutz, C., Wansing, H. (eds.) JELIA 2008. LNCS (LNAI), vol. 5293, pp. 1–4. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-87803-2_1

    Chapter  Google Scholar 

  8. Artemov, S.: The logic of justification. Rev. Symb. Log. 1(4), 477–513 (2008). https://doi.org/10.1017/s1755020308090060

    Article  MathSciNet  MATH  Google Scholar 

  9. Artemov, S.N.: Explicit provability and constructive semantics. Bull. Symb. Log. 7(1), 1–36 (2001). https://doi.org/10.2307/2687821

    Article  MathSciNet  MATH  Google Scholar 

  10. Artemov, S., Bonelli, E.: The intensional lambda calculus. In: Artemov, S.N., Nerode, A. (eds.) LFCS 2007. LNCS, vol. 4514, pp. 12–25. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-72734-7_2

    Chapter  Google Scholar 

  11. Asperti, A., Levy, J.J.: The cost of usage in the \(\lambda \)-calculus. In: Proceedings of 28th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2013, New Orleans, LA, June 2013, pp. 293–300. IEEE CS Press, Washington, DC (2013). https://doi.org/10.1109/lics.2013.35

  12. Banerjee, A., Naumann, D.A.: History-based access control and secure information flow. In: Barthe, G., Burdy, L., Huisman, M., Lanet, J.-L., Muntean, T. (eds.) CASSIS 2004. LNCS, vol. 3362, pp. 27–48. Springer, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30569-9_2

    Chapter  Google Scholar 

  13. Barendregt, H.P.: The Lambda Calculus: Its Syntax and Semantics. Studies in Logic and the Foundations of Mathematic, vol. 103, 2nd edn. North-Holland, Amsterdam (1984). https://www.sciencedirect.com/science/bookseries/0049-237X/103

    MATH  Google Scholar 

  14. Bavera, F., Bonelli, E.: Justification logic and audited computation. J. Log. Comput. 28(5), 909–934 (2018). https://doi.org/10.1093/logcom/exv037

    Article  MathSciNet  Google Scholar 

  15. de Bruijn, N.: Lambda-calculus notation with nameless dummies: a tool for automatic formula manipulation with application to the Church-Rosser theorem. Indagationes Math. 34(5), 381–392 (1972). https://doi.org/10.1016/1385-7258(72)90034-0

    Article  MathSciNet  MATH  Google Scholar 

  16. Garg, D., Jia, L., Datta, A.: Policy auditing over incomplete logs: theory, implementation and applications. In: Proceedings of 18th ACM Conference on Computer and Communications Security, CCS 2011, Chicago, IL, October 2011, pp. 151–162. ACM Press, New York (2011). https://doi.org/10.1145/2046707.2046726

  17. Giesl, J., et al.: Proving Termination of programs automatically with AProVE. In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 184–191. Springer, Cham (2014). https://doi.org/10.1007/978-3-319-08587-6_13

    Chapter  Google Scholar 

  18. Hardin, T.: Confluence results for the pure strong categorical combinatory logic CCL: \(\lambda \)-calculi as subsystems of CCL. Theor. Comput. Sci. 65(3), 291–342 (1989). https://doi.org/10.1016/0304-3975(89)90105-9

    Article  MATH  Google Scholar 

  19. Jia, L., et al.: AURA: a programming language for authorization and audit. In: Proceedings of 13th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, Victoria, BC, September 2008, pp. 27–38. ACM Press, New York (2008). https://doi.org/10.1145/1411204.1411212

  20. Kashima, R.: A proof of the standardization theorem in lambda-calculus. Technical report, Research Reports on Mathematical and Computing Science, Tokyo Institute of Technology (2000)

    Google Scholar 

  21. Moreau, L.: The foundations for provenance on the web. Found. Trends Web Sci. 2(2–3), 99–241 (2010). https://doi.org/10.1561/1800000010

    Article  Google Scholar 

  22. Perera, R., Acar, U.A., Cheney, J., Levy, P.B.: Functional programs that explain their work. In: Proceedings of 17th ACM SIGPLAN International Conference on Functional Programming, ICFP 2012, Copenhagen, September 2002, pp. 365–376. ACM Press, New York (2012). https://doi.org/10.1145/2364527.2364579

  23. Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511–540 (2001). https://doi.org/10.1017/s0960129501003322

    Article  MathSciNet  MATH  Google Scholar 

  24. Ricciotti, W.: A core calculus for provenance inspection. In: Proceedings of 19th International Symposium on Principles and Practice of Declarative Programming, PPDP 2017, Namur, October 2017, pp. 187–198. ACM Press, New York (2017). https://doi.org/10.1145/3131851.3131871

  25. Ricciotti, W., Cheney, J.: Strongly normalizing audited computation. In: Goranko, V., Dam, M. (eds.) Proceedings of 26th EACSL Annual Conference, CSL 2017, Stockholm, August 2017. Leibniz International Proceedings in Informatics, vol. 82, Article no. 36. Schloss Dagstuhl Publishing, Saarbrücken/Wadern (2017). https://doi.org/10.4230/lipics.csl.2017.36

  26. Ricciotti, W., Stolarek, J., Perera, R., Cheney, J.: Imperative functional programs that explain their work. Proc. ACM Program. Lang. 1(ICFP), Article no. 14 (2017). https://doi.org/10.1145/3110258

    Article  Google Scholar 

  27. Vaughan, J.A., Jia, L., Mazurak, K., Zdancewic, S.: Evidence-based audit. In: Proceedings of 21st IEEE Computer Security Foundations Symposium, CSF 2008, Pittsburgh, PA, June 2008, pp. 177–191. IEEE CS Press, Washington, DC (2008). https://doi.org/10.1109/csf.2008.24

  28. Xi, H.: Upper bounds for standardizations and an application. J. Symb. Log. 64(1), 291–303 (1999). https://doi.org/10.2307/2586765

    Article  MathSciNet  MATH  Google Scholar 

Download references

Acknowledgments

Effort sponsored by the Air Force Office of Scientific Research, Air Force Material Command, USAF, under grant number FA8655-13-1-3006. The U.S. Government and University of Edinburgh are authorised to reproduce and distribute reprints for their purposes notwithstanding any copyright notation thereon. Cheney was also supported by ERC Consolidator Grant Skye (grant number 682315). We are grateful to James McKinna and the anonymous reviewers for comments.

Author information

Authors and Affiliations

  1. LFCS, School of Informatics, University of Edinburgh, 10 Crichton Street, Edinburgh, EH8 9AB, UK

    Wilmer Ricciotti & James Cheney

Authors
  1. Wilmer Ricciotti
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. James Cheney
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Wilmer Ricciotti .

Editor information

Editors and Affiliations

  1. Stellenbosch University, Stellenbosch, South Africa

    Bernd Fischer

  2. Reykjavík University, Reykjavik, Iceland

    Tarmo Uustalu

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Ricciotti, W., Cheney, J. (2018). Explicit Auditing. In: Fischer, B., Uustalu, T. (eds) Theoretical Aspects of Computing – ICTAC 2018. ICTAC 2018. Lecture Notes in Computer Science(), vol 11187. Springer, Cham. https://doi.org/10.1007/978-3-030-02508-3_20

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-02508-3_20

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-02507-6

  • Online ISBN: 978-3-030-02508-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation