Explicit Auditing

  • Wilmer RicciottiEmail author
  • James Cheney
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11187)


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.


Lambda calculus Justification Logic Audited computation Explicit substitutions Abstract machines 



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.


  1. 1.
    Abadi, M., Cardelli, L., Curien, P.L., Lévy, J.J.: Explicit substitutions. J. Funct. Program. 1(4), 375–416 (1991). Scholar
  2. 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)
  3. 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).
  4. 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).
  5. 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). Scholar
  6. 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). Scholar
  7. 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). Scholar
  8. 8.
    Artemov, S.: The logic of justification. Rev. Symb. Log. 1(4), 477–513 (2008). Scholar
  9. 9.
    Artemov, S.N.: Explicit provability and constructive semantics. Bull. Symb. Log. 7(1), 1–36 (2001). Scholar
  10. 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). Scholar
  11. 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).
  12. 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). Scholar
  13. 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). Scholar
  14. 14.
    Bavera, F., Bonelli, E.: Justification logic and audited computation. J. Log. Comput. 28(5), 909–934 (2018). Scholar
  15. 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). Scholar
  16. 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).
  17. 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). Scholar
  18. 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). Scholar
  19. 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).
  20. 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. 21.
    Moreau, L.: The foundations for provenance on the web. Found. Trends Web Sci. 2(2–3), 99–241 (2010). Scholar
  22. 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).
  23. 23.
    Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Math. Struct. Comput. Sci. 11(4), 511–540 (2001). Scholar
  24. 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).
  25. 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).
  26. 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). Scholar
  27. 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).
  28. 28.
    Xi, H.: Upper bounds for standardizations and an application. J. Symb. Log. 64(1), 291–303 (1999). Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  1. 1.LFCS, School of InformaticsUniversity of EdinburghEdinburghUK

Personalised recommendations