Secrecy by Typing and File-Access Control

Avik Chaudhuri and Martín Abadi

Secrecy properties can be guaranteed through a combination of static and dynamic checks. The static checks may include the application of special type systems with notions of secrecy. The dynamic checks can be of many different kinds; in practice, the most important are access-control checks, often ones based on ACLs (access-control lists). In this paper, we explore the interplay of static and dynamic checks in the setting of a file system. For this purpose, we study a pi calculus with file-system constructs. The calculus supports both access-control checks and a form of static scoping that limits the knowledge of terms---including file names and contents---to groups of clients. We design a system with secrecy types for the calculus; using this system, we can prove secrecy properties by static typing of programs in the presence of file-system access-control checks.


    author = {Avik Chaudhuri and Mart\'{\i}n Abadi},
    title = {Secrecy by Typing and File-Access Control},
    booktitle = {Proceedings of the 19th IEEE Computer Security Foundations Workshop (CSFW'06)},
    year = {2006},
    pages = {112-123},
    publisher = {IEEE}