Deepak Garg

Papers and Reports

• A proof-carrying file system. Technical Report CMU-CS-09-123, 2009.
  Description of the design of PCFS, its use, and the logic BL.
  
  
• A logical representation of common rules for controlling access to classified information. Technical Report CMU-CS-09-139, 2009.
  A case study for the use of PCFS and BL.
  
  
• Proof-search in an authorization logic. Technical Report CMU-CS-09-121, 2009.
  Two methods for automatic proof search in BL. Generalization of one of these methods with time is implemented in PCFS.
  
  

Related Papers

• PCAL: Language support for proof-carrying authorization systems. European Symposium on Research in Computer Security (ESORICS), 2009. To appear.
  PCAL is a language that supports proof-carrying interfaces (including PCFS).
  
  
• An authorization logic with explicit time. IEEE Symposium on Computer Security Foundations (CSF), 2008. [Full version: Technical Report CMU-CS-07-166, 2007].
  Introduces explicit time, which is central to both BL and PCFS. The logic here is different from BL.
  
  
• Non-interference in constructive authorization logic. IEEE Computer Security Foundations Workshop (CSFW), 2006.
  Introduces proof-theory for access control. The logic is different from BL.