Document Open Access Logo

Strongly Normalizing Audited Computation

Authors Wilmer Ricciotti, James Cheney

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.36.pdf
  • Filesize: 0.72 MB
  • 21 pages

Document Identifiers

Author Details

Wilmer Ricciotti
James Cheney

Cite AsGet BibTex

Wilmer Ricciotti and James Cheney. Strongly Normalizing Audited Computation. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 36:1-36:21, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.36

Abstract

Auditing is an increasingly important operation for computer programming, for example in security (e.g. to enable history-based access control) and to enable reproducibility and accountability (e.g. provenance in scientific programming). Most proposed auditing techniques are ad hoc or treat auditing as a second-class, extralinguistic operation; logical or semantic foundations for auditing are not yet well-established. Justification Logic (JL) offers one such foundation; Bavera and Bonelli introduced a computational interpretation of JL called lambda^h that supports auditing. However, lambda^h is technically complex and strong normalization was only established for special cases. In addition, we show that the equational theory of lambda^h is inconsistent. We introduce a new calculus lambda^hc that is simpler than lambda^hc, consistent, and strongly normalizing. Our proof of strong normalization is formalized in Nominal Isabelle.
Keywords
  • lambda calculus
  • justification logic
  • strong normalization
  • audited computation

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. M. Abadi and C. Fournet. Access control based on execution history. In NDSS, 2003. Google Scholar
  2. Martín Abadi, Michael Burrows, Butler Lampson, and Gordon Plotkin. A calculus for access control in distributed systems. ACM Trans. Program. Lang. Syst., 15(4), 1993. URL: http://dx.doi.org/10.1145/155183.155225.
  3. U. A. Acar, A. Ahmed, J. Cheney, and R. Perera. A core calculus for provenance. Journal of Computer Security, 21:919-969, 2013. URL: http://dx.doi.org/10.1007/978-3-642-28641-4_22.
  4. S. Amir-Mohammadian, S. Chong, and C. Skalka. Correct audit logging: Theory and practice. In POST, pages 139-162, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49635-0_8.
  5. S. Artemov. The logic of justification. Review of Symbolic Logic, 1(4):477-513, 2008. URL: http://dx.doi.org/10.1017/S1755020308090060.
  6. S. N. Artëmov. Explicit provability and constructive semantics. Bulletin of Symbolic Logic, 7(1):1-36, 2001. URL: http://dx.doi.org/10.2307/2687821.
  7. S. N. Artëmov and E. Bonelli. The intensional lambda calculus. In Logical Foundations of Computer Science, pages 12-25, 2007. URL: http://dx.doi.org/10.1007/978-3-540-72734-7_2.
  8. Federico Aschieri and Margherita Zorzi. Non-determinism, non-termination and the strong normalization of System T. In TLCA, pages 31-47, 2013. URL: http://dx.doi.org/10.1007/978-3-642-38946-7_5.
  9. F. Bavera and E. Bonelli. Justification logic and audited computation. Journal of Logic and Computation, 2015. Published online, June 19, 2015. URL: http://dx.doi.org/10.1093/logcom/exv037.
  10. J. Cheney. A formal framework for provenance security. In Proceedings of the 24th IEEE Computer Security Foundations Symposium (CSF), pages 281-293. IEEE, 2011. URL: http://dx.doi.org/10.1109/CSF.2011.26.
  11. J. H. Gallier. On Girard’s "candidats de réductibilité". In Logic and Computer Science, pages 123-203. Academic Press, 1990. Google Scholar
  12. H. Geuvers. A short and flexible proof of strong normalization for the calculus of constructions. In Selected Papers from TYPES'94, LNCS, pages 14-38. Springer-Verlag, 1995. URL: http://dx.doi.org/10.1007/3-540-60579-7_2.
  13. J.-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In Scandinavian Logic Symposium, 1978, pages 63-92. North-Holland, 1971. Google Scholar
  14. J.-Y. Girard, P. Taylor, and Y. Lafont. Proofs and Types. Cambridge University Press, New York, NY, USA, 1989. Google Scholar
  15. L. Jia, J. A. Vaughan, K. Mazurak, J. Zhao, L. Zarko, J. Schorr, and S. Zdancewic. Aura: a programming language for authorization and audit. In ICFP, pages 27-38, 2008. URL: http://dx.doi.org/10.1145/1411204.1411212.
  16. C. I. Lewis. Symbolic Logic. Dover Publications, 1959. Google Scholar
  17. Sam Lindley and Ian Stark. Reducibility and ⊤-lifting for computation types. In TLCA, number 3461 in LNCS, pages 262-277. Springer-Verlag, 2005. URL: http://dx.doi.org/10.1007/11417170_20.
  18. Z. Luo. An Extended Calculus of Constructions. PhD thesis, University of Edinburgh, 1990. Google Scholar
  19. M. Parigot. Strong normalization for the second order classical natural deduction. In Proceedings of LICS, 1994. Google Scholar
  20. R. Perera, U. A. Acar, J. Cheney, and P. B. Levy. Functional programs that explain their work. In ICFP, pages 365-376. ACM, 2012. URL: http://dx.doi.org/10.1145/2398856.2364579.
  21. F. Pfenning and R. Davies. A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science, 11(4):511-540, 2001. URL: http://dx.doi.org/10.1017/S0960129501003322.
  22. Colin Riba. On the stability by union of reducibility candidates. In FOSSACS, pages 317-331, Berlin, Heidelberg, 2007. Springer-Verlag. URL: http://dx.doi.org/10.1007/978-3-540-71389-0_23.
  23. W. W. Tait. A realizability interpretation of the theory of species. In Logic Colloquium, 1972-73, volume 453 of Lecture Notes in Mathematics, pages 240-251. Springer, 1975. URL: http://dx.doi.org/10.1007/BFb0064875.
  24. J. A. Vaughan, L. Jia, K. Mazurak, and S. Zdancewic. Evidence-based audit. In CSF, pages 177-191, 2008. URL: http://dx.doi.org/10.1109/CSF.2008.24.
  25. B. Werner. Une Théorie des Constructions Inductives. PhD thesis, Université Paris VII, 1994. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact