First-Order Logic for Flow-Limited Authorization

January 28, 2020 · Entered Twilight · 🏛 IEEE Computer Security Foundations Symposium

"Last commit was 6.0 years ago (≥5 year threshold)"

Evidence collected by the PWNC Scanner

Repo contents: Base, CoqMakefile.conf, Logic, Makefile, Makefile.conf, README, Security, Tactics, _CoqProject

Authors Andrew K. Hirsch, Pedro H. Azevedo de Amorim, Ethan Cecchetti, Ross Tate, Owen Arden arXiv ID 2001.10630 Category cs.CR: Cryptography & Security Cross-listed cs.LO, cs.PL Citations 5 Venue IEEE Computer Security Foundations Symposium Repository https://github.com/FLAFOL/flafol-coq Last Checked 4 months ago

Abstract

We present the Flow-Limited Authorization First-Order Logic (FLAFOL), a logic for reasoning about authorization decisions in the presence of information-flow policies. We formalize the FLAFOL proof system, characterize its proof-theoretic properties, and develop its security guarantees. In particular, FLAFOL is the first logic to provide a non-interference guarantee while supporting all connectives of first-order logic. Furthermore, this guarantee is the first to combine the notions of non-interference from both authorization logic and information-flow systems. All theorems in this paper are proven in Coq.