Secrecy by Typing and File-Access Control

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.

• Type: Conference
• Year: 2006
• Where: CSFW
• Authors: Avik Chaudhuri, Martín Abadi
• Keywords: Access-control Checks, CSFW 2006, Dynamic Checks, Secrecy Properties, Security Privacy