Deepak Garg

Research Papers

Published Papers

• Groundhog: Efficient Request Isolation in FaaS. With Mohamed Alzayat, Jonathan Mace and Peter Druschel. European Conference on Computer Systems (EuroSys), 2023.
• DimSum: A Decentralized Approach to Multi-language Semantics and Verification. With Michael Sammler, Simon Spies, Youngju Song, Emanuele D'Osualdo, Robbert Krebbers and Derek Dreyer. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2023. [Appendix] [Webpage with Coq code]  Distinguished paper 
• BFF: Foundational and Automatic Verification of Bitfield-Manipulating Programs. With Fengmin Zhu, Michael Sammler, Rodolphe Lepigre and Derek Dreyer. OOPSLA, 2022. [Webpage with Coq code]
• SecurePtrs: Proving Secure Compilation Using Data-Flow Back-Translation and Turn-Taking Simulation. With Akram El-Korashy, Roberto Blanco, Jeremy Thibault, Adrien Durier and Catalin Hritcu. IEEE Symposium on Computer Security Foundations (CSF), 2022.
• Islaris: Verification of Machine Code Against Authoritative ISA Semantics. With Michael Sammler, Angus Hammond, Rodolphe Lepigre, Brian Campbell, Jean Pichon-Pharabod, Derek Dreyer and Peter Sewell. Programming Language Design and Implementation (PLDI), 2022.
• Listening to Bluetooth Beacons for Epidemic Risk Mitigation. With Gilles Barthe, Roberta De Viti, Peter Druschel, Manuel Gomez-Rodriguez, Heiner Kremer, Pierfrancesco Ingo, Matthew Lentz, Lars Lorch, Aastha Mehta and Bernhard Schölkopf. Nature Scientific Reports, 2022. [Related system design paper: arXiv]
• Pacer: Comprehensive Network Side-Channel Mitigation in the Cloud. With Aastha Mehta, Mohamed Alzayat, Roberta De Viti, Björn Brandenburg and Peter Druschel. USENIX Security Symposium, 2022. [Technical report]
• Pirouette: Higher-order typed functional choreographies. With Andrew K. Hirsch. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2022. [Full version]  Distinguished paper 
• Isolation Without Taxation. With Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Ranjit Jhala and Deian Stefan. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2022. [Full version]
• Relational cost analysis for functional-imperative programs. With Weihao Qu and Marco Gaboardi. Journal of Functional Programming, 2021.
• Higher-Order probabilistic adversarial computations: Categorical semantics and program logics. With Alejandro Aguirre, Gilles Barthe, Marco Gaboardi, Shin-ya Katsumata and Tetsuya Sato. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2021.
• RefinedC: Automating the Foundational Verification of C Code with Refined Ownership Types. With Michael Sammler, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian and Derek Dreyer. Programming Language Design and Implementation (PLDI), 2021.  Distinguished paper  and  Distinguished artifact award . [Webpage with appendix and implementation]
• CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle. With Akram El-Korashy, Stelios Tsampas, Marco Patrignani, Dominique Devriese and Frank Piessens. IEEE Symposium on Computer Security Foundations (CSF), 2021. [Technical appendix with proofs]
• Permissive runtime information flow control in the presence of exceptions. With Abhishek Bichhawat, Vineet Rajani and Christian Hammer. Journal of Computer Security, 2021.
• An Extended Account of Trace-Relating Compiler Correctness and Secure Compilation. With Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Catalin Hritcu, Marco Patrignani, Eric Tanter and Jeremy Thibault. ACM Transactions on Programming Languages and Systems (TOPLAS), 2021.
• Robustly Safe Compilation, an Efficient Form of Secure Compilation. With Marco Patrignani. ACM Transactions on Programming Languages and Systems (TOPLAS), 2021. [Technical appendix with proofs]
• A unifying type-theory for higher-order (amortized) cost analysis. With Vineet Rajani, Marco Gaboardi and Jan Hoffmann. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2021. [Technical appendix with proofs]
• Accountability in the Decentralised-Adversary Setting. With Robert Kuennemann and Michael Backes. IEEE Symposium on Computer Security Foundations (CSF), 2021.
• Trace-relating compiler correctness and secure compilation. With Carmine Abate, Roberto Blanco, Stefan Ciobaca, Adrien Durier, Catalin Hritcu, Marco Patrignani, Eric Tanter and Jeremy Thibault. European Symposium on Programming (ESOP), 2020. [Full version with appendix. Also available here: arXiv:1907.05320] Superseded by the TOPLAS 2021 paper
• Finding safety in numbers with secure allegation escrows. With Venkat Arun, Aniket Kate, Peter Druschel and Bobby Bhattacharjee. Network and Distributed Security Symposium (NDSS), 2020.
• On the expressiveness and semantics of information flow types. With Vineet Rajani. Journal of Computer Security, 2020. [Appendix]
• The high-level benefits of low-level sandboxing. With Michael Sammler, Derek Dryer and Tadeusz Litak. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2020. [Coq artifact with proofs]
• A relational logic for higher-order programs. With Alejandro Aguirre, Gilles Barthe, Marco Gaboardi and Pierre-Yves Strub. Journal of Functional Programming, 2019. [Official version]
• Relational cost analysis for functional-imperative programs. With Weihao Qu and Marco Gaboardi. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2019. [Appendix] Superseded by the JFP 2021 paper
• ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK). With Anjo Vahldiek-Oberwagner, Eslam Elnikety, Nuno Duarte, Michael Sammler and Peter Druschel. USENIX Security Symposium, 2019.  Distinguished paper  and  Internet Defense Prize .
• Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation. With Carmine Abate, Roberto Blanco, Catalin Hritcu, Marco Patrignani and Jérémy Thibault. IEEE Symposium on Computer Security Foundations (CSF), 2019.  Distinguished paper . [Full version with appendix. Also available here: https://arxiv.org/abs/1807.04603]
• Bidirectional Type Checking for Relational Properties. With Ezgi Cicek, Weihao Qu, Gilles Barthe and Marco Gaboardi. Programming Language Design and Implementation (PLDI), 2019. [Appendix]
• Composing abstractions using the null-kernel. With James Litton, Peter Druschel and Bobby Bhattacharjee. HotOS XVII, 2019.
• Robustly Safe Compilation. With Marco Patrignani. European Symposium on Programming (ESOP), 2019. [Appendix] Superseded by the TOPLAS 2021 paper
• CONFLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code. With Ajay Brahmakshatriya, Piyus Kedia, Hamed Nemati, Derrick McKee, Akash Lal, Aseem Rastogi, Anmol Panda and Pratik Bhatu. European Conference on Computer Systems (EuroSys), 2019. [Full version with appendix]
• From fine- to coarse-grained dynamic information flow control and back. With Marco Vassena, Alejandro Russo, Vineet Rajani and Deian Stefan. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019.  Distinguished paper .
• Formal verification of higher-order probabilistic programs. With Tetsuya Sato, Alejandro Aguirre, Gilles Barthe, Marco Gaboardi and Justin Hsu. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2019.
• Types for Information Flow Control: Labeling Granularity and Semantic Models. With Vineet Rajani. IEEE Symposium on Computer Security Foundations (CSF), 2018.  Distinguished paper . [Appendix] Superseded by the JCS 2020 paper
• UniTraX: Protecting Data Privacy with Discoverable Biases. With Reinhard Munz, Fabienne Eigner, Matteo Maffei and Paul Francis. Conference on Principles of Security and Trust (POST), 2018. [Technical report with proofs]
• Relational reasoning for Markov chains in a probabilistic guarded lambda calculus. With Alejandro Aguirre, Gilles Barthe, Lars Birkedal, Aleš Bizjak and Marco Gaboardi. European Symposium on Programming (ESOP), 2018. [Full version with appendix]
• Monadic refinements for relational cost analysis. With Ivan Radicek, Gilles Barthe, Marco Gaboardi and Florian Zuleger. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2018. [Appendix]
• Robust and compositional verification of object capability patterns. With Dave Swasey and Derek Dreyer. OOPSLA, 2017.  Distinguished paper award . [Long version with appendix] [Coq development]
• WebPol: Fine-grained information flow policies for web browsers. With Abhishek Bichhawat, Vineet Rajani, Jinank Jain and Christian Hammer. European Symposium on Research in Computer Security (ESORICS), 2017. [Full version with appendix: arXiv:1706.06932]
• A relational logic for higher-order programs. With Alejandro Aguirre, Gilles Barthe, Marco Gaboardi and Pierre-Yves Strub. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2017. [Post-conference version with minor typo fixes] [Appendix with proofs and all proof rules] Superseded by the JFP 2019 paper
• Secure compilation and hyperproperty preservation. With Marco Patrignani. IEEE Symposium on Computer Security Foundations (CSF), 2017.
• Qapla: Policy compliance for database-backed systems. With Aastha Mehta, Eslam Elnikety, Katura Harvey and Peter Druschel. USENIX Security Symposium, 2017.
• Type Systems for Information Flow Control: The Question of Granularity. With Vineet Rajani, Iulia Bastys and Willard Rafnsson. Invited article in ACM SIGLOG News, 2017. [Full version with proofs: Technical Report MPI-SWS-2016-012] Superseded by the CSF 2018 paper.
• Relational Cost Analysis. With Ezgi Cicek, Gilles Barthe, Marco Gaboardi and Jan Hoffmann. ACM SIGPLAN Symposium on Principles of Programming Languages (POPL), 2017. [Appendix with proofs]
• Light-weight Contexts: An OS Abstraction for Safety and Performance. With James Litton, Anjo Vahldiek-Oberwagner, Eslam Elnikety, Bobby Bhattacharjee and Peter Druschel. USENIX Symposium on Operating Systems Design and Implementation (OSDI), 2016.
• A type theory for incremental computational complexity with control flow changes. With Ezgi Cicek and Zoe Paraskevopoulou. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2016. [Appendix with proofs]
• Thoth: Comprehensive policy compliance in data retrieval systems. With Eslam Elnikety, Aastha Mehta, Anjo Vahldiek-Oberwagner and Peter Druschel. USENIX Security Symposium, 2016.
• Causally consistent dynamic slicing. With Roly Perera and James Cheney. International Conference on Concurrency Theory (CONCUR), 2016.
• On capabilities, access control, their equivalence and confused deputy attacks. With Vineet Rajani and Tamara Rezk. IEEE Symposium on Computer Security Foundations (CSF), 2016. [Technical appendix with proofs]
• Asymmetric Secure Multi-execution with Declassification. With Iulia Bolosteanu. Conference on Principles of Security and Trust (POST), 2016. [Full version with appendix] © Springer-Verlag
• Progress-Sensitive Security for SPARK. With Willard Rafnsson and Andrei Sabelfeld. International Symposium on Engineering Secure Software and Systems (ESSoS), 2016. [Full version with appendix] © Springer-Verlag
• Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits. With Omar Chowdhury, Limin Jia and Anupam Datta. ACM Conference on Computer and Communications Security (CCS), 2015.
• Information Flow Control for Event Handling and the DOM in Web Browsers. With Vineet Rajani, Abhishek Bichhawat and Christian Hammer. IEEE Symposium on Computer Security Foundations (CSF), 2015.  RS3 best paper award . [Full version with appendix] [OCaml model of the DOM with information flow control instrumentation (15 KB tgz)]
• A Logic of Programs with Interface-confined Code. With Limin Jia, Shayak Sen and Anupam Datta. IEEE Symposium on Computer Security Foundations (CSF), 2015. [Full version with appendix: arXiv:1501.05673]
• Program Actions as Actual Causes: A Building Block for Accountability. With Anupam Datta, Dilsun Kaynar, Divya Sharma and Arunesh Sinha. IEEE Symposium on Computer Security Foundations (CSF), 2015. [Full version with appendix: arXiv:1505.01131, PDF]
• Guardat: Enforcing Data Policies at the Storage Layer. With Anjo Vahldiek-Oberwagner, Eslam Elnikety, Aastha Mehta, Peter Druschel, Rodrigo Rodrigues, Johannes Gehrke and Ansley Post. European Conference on Computer Systems (EuroSys), 2015.
• Refinement Types for Incremental Computational Complexity. With Ezgi Cicek and Umut Acar. European Symposium on Programming (ESOP), 2015. [Appendix with proofs] © Springer-Verlag
• Temporal Mode-Checking for Runtime Monitoring of Privacy Policies. With Omar Chowdhury, Limin Jia and Anupam Datta. International Conference on Computer Aided Verification (CAV), 2014. [Full version with proofs] © Springer-Verlag
• Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis. With Abhishek Bichhawat, Vineet Rajani and Christian Hammer. ACM Workshop on Programming Languages and Analysis for Security (PLAS), 2014. [Full version with proofs and a minor improvement] Paper also appears in the informal proceedings of FCS-FCC 2014. © ACM
• Information Flow Control in WebKit's JavaScript Bytecode. With Abhishek Bichhawat, Vineet Rajani and Christian Hammer. Conference on Principles of Security and Trust (POST), 2014. [Full version with proofs] © Springer-Verlag
• Privacy-Preserving Audit for Broker-Based Health Information Exchange. With Se Eun Oh, Ji Young Chun, Limin Jia, Carl A. Gunter and Anupam Datta. ACM Conference on Data and Application Security and Privacy (CODASPY), 2014. © ACM
• Dependent Type Theory for Verification of Information Flow and Access Control Policies. With Aleks Nanevski and Anindya Banerjee. ACM Transactions on Programming Languages and Systems (TOPLAS), 2013. © ACM
• Stateful Authorization Logic - Proof Theory and A Case Study. With Frank Pfenning. Journal of Computer Security, Vol. 20, 2012. © IOS Press
• Superficially Substructural Types. With Neelakantan Krishnaswami, Aaron Turon and Derek Dreyer. ACM SIGPLAN International Conference on Functional Programming (ICFP), 2012. [Technical appendix with proofs] © ACM
• Labeled Goal-directed Search in Access Control Logic. With Valerio Genovese and Daniele Rispoli. International Workshop on Security and Trust Management (STM), 2012. [Full version with proofs] © Springer-Verlag
• Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction. With Valerio Genovese and Daniele Rispoli. IEEE Symposium on Computer Security Foundations (CSF), 2012. [Full version with proofs] © IEEE
• Countermodels from Sequent Calculi in Multi-Modal Logics. With Valerio Genovese and Sara Negri. ACM/IEEE Symposium on Logic in Computer Science (LICS), 2012. [Full version with proofs] © IEEE
• Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms. With Anupam Datta, Jeremiah Blocki, Nicolas Christin, Henry DeYoung, Limin Jia, Dilsun Kaynar and Arunesh Sinha. Invited to the International Conference on Information Systems Security (ICISS), 2011. © Springer-Verlag
• Policy Auditing over Incomplete Logs: Theory, Implementation and Applications. With Limin Jia and Anupam Datta. ACM Conference on Computer and Communications Security (CCS), 2011. [Implementation (10 MB tgz)] [Full version with proofs: Technical Report CMU-CyLab-11-002 and arXiv.org:1102.2521v3] © ACM
• A Proof-Carrying File System with Revocable and Use-Once Certificates. With Jamie Morgenstern and Frank Pfenning. International Workshop on Security and Trust Management (STM), 2011. © Springer-Verlag
• New Modalities for Access Control Logics: Permission, Control and Ratification. With Valerio Genovese. International Workshop on Security and Trust Management (STM), 2011. [Full version with proofs] © Springer-Verlag
• Verification of Information Flow and Access Control Policies via Dependent Types. With Aleks Nanevski and Anindya Banerjee. IEEE Symposium on Security and Privacy (Oakland), 2011. [Full version: Technical report IMDEA-SW-TR-2010.0]. Expanded version in TOPLAS 2013. © IEEE
• On Adversary Models and Compositional Security. With Anupam Datta, Jason Franklin, Limin Jia and Dilsun Kaynar. IEEE Security and Privacy Magazine, special issue on the Science of Security, 2011. © IEEE
• Experiences in the logical specification of the HIPAA and GLBA privacy laws. With Henry DeYoung, Limin Jia, Dilsun Kaynar, and Anupam Datta. Workshop on Privacy in the Electronic Society (WPES), 2010. [Full version: Technical report CMU-CyLab-10-007] © ACM
• Stateful authorization logic - proof theory and a case study. With Frank Pfenning. International Workshop on Security and Trust Management (STM), LNCS Volume 6710, 2010. For details and proofs see chapters 4 and 8 of my dissertation. Superseded by the Journal of Computer Security 2012 paper © Springer-Verlag
• Compositional system security with interface-confined adversaries. With Jason Franklin, Dilsun Kaynar, and Anupam Datta. Electronic Notes in Theoretical Computer Science (ENTCS), Volume 265: Proceedings of the 26th Conference on Mathematical Foundations of Programming Semantics (MFPS), 2010. [Full version: Technical Report CMU-CyLab-10-004] © Elsevier
• A proof-carrying file system. With Frank Pfenning. IEEE Symposium on Security and Privacy (Oakland), 2010. [Implementation] [Expanded, outdated version: Technical Report CMU-CS-09-123] For details and proofs see chapters 4, 5 and 7 of my dissertation. © IEEE
• PCAL: Language support for proof-carrying authorization systems. With Avik Chaudhuri. European Symposium on Research in Computer Security (ESORICS), 2009. [Full version: Technical Report CMU-CS-09-141] © Springer-Verlag
• A logic of secure systems and its application to trusted computing. With Anupam Datta, Jason Franklin and Dilsun Kaynar. IEEE Symposium on Security and Privacy (Oakland), 2009. [Full version: Technical Report CMU-CyLab-09-001] © IEEE
• An authorization logic with explicit time. With Henry DeYoung and Frank Pfenning. IEEE Symposium on Computer Security Foundations (CSF), 2008. [Full version: Technical Report CMU-CS-07-166, 2007] © IEEE
• Principal-centric reasoning in constructive authorization logic. Workshop on Intuitionistic Modal Logic and Applications (IMLA), 2008. [Full version: Technical Report CMU-CS-09-120, 2009]
• A logic for reasoning about networked secure systems. With Anupam Datta, Jason Franklin and Dilsun Kaynar. FCS-ARSPA-WITS Workshop, 2008. [Full version with proofs] Superseded by the Oakland 2009 paper.
• A modal deconstruction of access control logics. With Martín Abadi. International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), 2008. [Full version with proofs] © Springer-Verlag
• Consumable credentials in logic-based access-control systems. With Kevin D. Bowers, Lujo Bauer, Frank Pfenning and Michael K. Reiter. Network & Distributed System Security Symposium (NDSS), 2007.
• A linear logic of authorization and knowledge. With Lujo Bauer, Kevin D. Bowers, Frank Pfenning and Michael K. Reiter. European Symposium on Research in Computer Security (ESORICS), 2006. [Extended version] © Springer-Verlag
• Non-interference in constructive authorization logic. With Frank Pfenning. IEEE Computer Security Foundations Workshop (CSFW), 2006. © IEEE
• Type-directed concurrency. With Frank Pfenning. International Conference on Concurrency Theory (CONCUR), 2005. [Full version: Technical Report CMU-CS-05-104] © Springer-Verlag
• Effective chemistry for synchrony and asynchrony. With Akash Lal and Sanjiva Prasad. IFIP International Conference on Theoretical Computer Science (IFIP-TCS), 2004. © Kluwer

Edited Volumes

• Proceedings of the 15th International Conference on Information Systems Security (ICISS 2019). Editors Deepak Garg, N. V. Narendra Kumar and Rudrapatna K. Shyamasundar. © Springer
• Proceedings of the 5th ACM SIGPLAN Workshop on Programming Languages and Analysis of Security (PLAS 2010). Editors Anindya Banerjee and Deepak Garg. June, 2010. ISBN: 978-1-60558-827-8. © ACM

Theses

• Proof Theory for Authorization Logic and Its Application to a Practical File System. Ph.D. Dissertation, 2009. Available as Technical Report CMU-CS-09-168. [Typeset for: Letter size, A4 size] [Implementation]

Technical Reports

• Privacy policy specification and audit in a fixed-point logic - How to enforce HIPAA, GLBA and all that. With Henry DeYoung, Limin Jia, Dilsun Kaynar, and Anupam Datta. Technical report CMU-CyLab-10-008, 2010.
• A logical representation of common rules for controlling access to classified information. With Frank Pfenning, Denis Serenyi and Brian Witten. Technical Report CMU-CS-09-139, 2009.
• Proof-search in an authorization logic. Technical Report CMU-CS-09-121, 2009.
• Towards a theory of secure systems. With Anupam Datta, Jason Franklin and Dilsun Kaynar. Technical Report CMU-CyLab-08-003, 2008. Superseded by the Oakland 2009 paper.
• From indexed lax logic to intuitionistic logic. With Michael Carl Tschantz. Technical Report CMU-CS-07-167, 2007.

Notes/Misc/Drafts

• Typed language support for proof-carrying authorization. Notes for 18-739: Foundations of Security and Privacy. November, 2009.
• An introduction to proof-carrying authorization. Notes for 18-739: Foundations of Security and Privacy. December, 2007.

Imprint / Data Protection