Deepak Garg
Research Papers
[Published papers]
[Edited volumes]
[Theses]
[Technical reports]
[Notes and misc]
[Arranged by: Date | Topic]
Published papers may be copyrights of their respective
publishers.
Type/logic-based verification
-
Program
Analysis for Adaptive Data Analysis. With Jiawen Liu,
Weihao Qu, Marco Gaboardi and Jonathan
R. Ullman. Programming Language Design and
Implementation (PLDI), 2024.
-
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]
-
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.
-
Pirouette: Higher-order
typed functional choreographies. With Andrew
K. Hirsch. ACM SIGPLAN Symposium on Principles of
Programming Languages (POPL),
2022. [Full
version] Distinguished
paper
-
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]
-
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]
-
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
-
Bidirectional Type Checking for
Relational Properties. With Ezgi Cicek, Weihao Qu, Gilles
Barthe and Marco Gaboardi. Programming Language Design and
Implementation (PLDI),
2019. [Appendix]
-
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.
-
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]
-
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
-
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]
-
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]
-
Refinement Types for Incremental
Computational Complexity. With Ezgi Cicek and Umut
Acar. European Symposium on Programming (ESOP),
2015. [Appendix
with proofs] © Springer-Verlag
-
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
-
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
-
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
Software and OS security
-
Toast:
A Heterogeneous Memory Management System. With Maurice
Bailleu, Dimitrios Stavrakakis, Rodrigo Caetano Rocha, Soham
Chakraborty and Pramod Bhatotia.
Proceedings of the 2024 International Conference on
Parallel Architectures and Compilation Techniques (PACT),
2024.
-
Blueprint: A Toolchain for Highly-Reconfigurable
Microservices. With Vaastav Anand, Antoine Kaufmann and Jonathan Mace. ACM Symposium on Operating Systems Principles (SOSP), 2023.
-
Groundhog: Efficient
Request Isolation in FaaS. With Mohamed Alzayat, Jonathan
Mace and Peter Druschel. European Conference on Computer
Systems (EuroSys), 2023.
-
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]
-
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]
-
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 .
-
Composing abstractions using the
null-kernel. With James Litton, Peter Druschel and Bobby
Bhattacharjee. HotOS XVII, 2019.
-
Qapla: Policy compliance for
database-backed systems. With Aastha Mehta, Eslam
Elnikety, Katura Harvey and Peter Druschel. USENIX Security
Symposium, 2017.
-
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.
-
Thoth: Comprehensive policy compliance in
data retrieval systems. With Eslam Elnikety, Aastha Mehta,
Anjo Vahldiek-Oberwagner and Peter Druschel. USENIX
Security Symposium, 2016.
-
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.
-
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
- 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
-
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.
Secure compilation
-
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.
-
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]
-
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]
-
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
-
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]
-
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]
-
Secure compilation and
hyperproperty preservation. With Marco Patrignani. IEEE
Symposium on Computer Security Foundations (CSF), 2017.
Language-based information flow control
-
From
Fine- to Coarse-Grained Dynamic Information Flow Control and
Back. With Marco Vassena, Alejando Russo, Vineet Rajani
and Deian Stefan. Foundations and Trends in Programming
Languages, Vol. 8, Issue 1, 2023. Extended version of
the POPL 2019 paper.
-
Compositional Security Definitions for Higher-Order Where
Declassification. With Jan Menz, Andrew K. Hirsch and Peixuan Li. OOPSLA, 2023. [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.
-
On the expressiveness and semantics of
information flow types. With Vineet Rajani. Journal of
Computer Security,
2020. [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 .
-
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
-
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]
-
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.
-
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
-
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)]
-
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
Distributed secure and private computation
-
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]
-
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.
Differential privacy
Privacy policies and audit
-
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.
-
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
-
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
-
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
- 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
Causal analysis
Verification of security properties
-
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]
- 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
-
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 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
-
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.
Proof theory (including logics for access control)
-
Stateful Authorization Logic
- Proof Theory and A Case Study. With Frank
Pfenning. Journal of Computer Security,
Vol. 20, 2012. © IOS Press
-
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
-
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
-
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
-
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
-
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 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
-
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
Concurrency theory
Technical reports related to published papers are listed
above with their respective papers.
-
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.
These are unpublished notes or drafts. They are provided
as is. Please do not cite them.
Imprint
/ Data
Protection