Secrecy by Typing and File-Access Control

9 years 2 months ago
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.
Avik Chaudhuri, Martín Abadi
Added 10 Jun 2010
Updated 10 Jun 2010
Type Conference
Year 2006
Where CSFW
Authors Avik Chaudhuri, Martín Abadi
Comments (0)