Deepak Garg

ACM Trans. Program. Lang. Syst., 2021

An Extended Account of Trace-relating Compiler Correctness and Secure Compilation.

[BibT_eX]

[DOI]

ACM Trans. Program. Lang. Syst., 2021

A unifying type-theory for higher-order (amortized) cost analysis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Higher-order probabilistic adversarial computations: categorical semantics and program logics.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2021

Relational cost analysis in a functional-imperative setting.

[BibT_eX]

[DOI]

Weihao Qu

Marco Gaboardi

J. Funct. Program., 2021

Permissive runtime information flow control in the presence of exceptions.

[BibT_eX]

[DOI]

J. Comput. Secur., 2021

Secure Compilation (Dagstuhl Seminar 21481).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2021

Isolation Without Taxation: Near Zero Cost Transitions for SFI.

[BibT_eX]

[DOI]

CoRR, 2021

RefinedC: automating the foundational verification of C code with refined ownership types.

[BibT_eX]

[DOI]

Proceedings of the PLDI '21: 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021

Accountability in the Decentralised-Adversary Setting.

[BibT_eX]

[DOI]

Robert Künnemann

Michael Backes

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

CapablePtrs: Securely Compiling Partial Programs Using the Pointers-as-Capabilities Principle.

[BibT_eX]

[DOI]

Proceedings of the 34th IEEE Computer Security Foundations Symposium, 2021

2020

The high-level benefits of low-level sandboxing.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2020

On the expressiveness and semantics of information flow types.

[BibT_eX]

[DOI]

Vineet Rajani

J. Comput. Secur., 2020

PanCast: Listening to Bluetooth Beacons for Epidemic Risk Mitigation.

[BibT_eX]

[DOI]

Manuel Gomez-Rodriguez

CoRR, 2020

Finding Safety in Numbers with Secure Allegation Escrows.

[BibT_eX]

[DOI]

Proceedings of the 27th Annual Network and Distributed System Security Symposium, 2020

Trace-Relating Compiler Correctness and Secure Compilation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2020

2019

Formal verification of higher-order probabilistic programs: reasoning about approximation, convergence, Bayesian inference, and optimization.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2019

Relational cost analysis for functional-imperative programs.

[BibT_eX]

[DOI]

Weihao Qu

Marco Gaboardi

Proc. ACM Program. Lang., 2019

Causality & Control Flow.

[BibT_eX]

[DOI]

Robert Künnemann

Michael Backes

Proceedings of the 4th Workshop on Formal Reasoning about Causation, 2019

Pacer: Network Side-Channel Mitigation in the Cloud.

[BibT_eX]

[DOI]

CoRR, 2019

Trace-Relating Compiler Correctness and Secure Compilation.

[BibT_eX]

[DOI]

CoRR, 2019

ERIM: Secure, Efficient In-process Isolation with Protection Keys (MPK).

[BibT_eX]

[DOI]

Proceedings of the 28th USENIX Security Symposium, 2019

Bidirectional type checking for relational properties.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Composing Abstractions using the null-Kernel.

[BibT_eX]

[DOI]

Proceedings of the Workshop on Hot Topics in Operating Systems, 2019

ConfLLVM: A Compiler for Enforcing Data Confidentiality in Low-Level Code.

[BibT_eX]

[DOI]

Proceedings of the Fourteenth EuroSys Conference 2019, Dresden, Germany, March 25-28, 2019, 2019

Robustly Safe Compilation.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2019

Journey Beyond Full Abstraction: Exploring Robust Property Preservation for Secure Compilation.

[BibT_eX]

[DOI]

Proceedings of the 32nd IEEE Computer Security Foundations Symposium, 2019

2018

Monadic refinements for relational cost analysis.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2018

Accountability in Security Protocols.

[BibT_eX]

[DOI]

Robert Künnemann

Michael Backes

IACR Cryptol. ePrint Arch., 2018

Secure Compilation (Dagstuhl Seminar 18201).

[BibT_eX]

[DOI]

Dagstuhl Reports, 2018

SATE: Robust and Private Allegation Escrows.

[BibT_eX]

[DOI]

CoRR, 2018

Formal verification of higher-order probabilistic programs.

[BibT_eX]

[DOI]

CoRR, 2018

Exploring Robust Property Preservation for Secure Compilation.

[BibT_eX]

[DOI]

CoRR, 2018

Robustly Safe Compilation or, Efficient, Provably Secure Compilation.

[BibT_eX]

[DOI]

CoRR, 2018

ERIM: Secure and Efficient In-process Isolation with Memory Protection Keys.

[BibT_eX]

[DOI]

Eslam Elnikety

Peter Druschel

CoRR, 2018

Shai: Enforcing Data-Specific Policies with Near-Zero Runtime Overhead.

[BibT_eX]

[DOI]

Eslam Elnikety

Peter Druschel

CoRR, 2018

UniTraX: Protecting Data Privacy with Discoverable Biases.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - 7th International Conference, 2018

Relational Reasoning for Markov Chains in a Probabilistic Guarded Lambda Calculus.

[BibT_eX]

[DOI]

Proceedings of the Programming Languages and Systems, 2018

Types for Information Flow Control: Labeling Granularity and Semantic Models.

[BibT_eX]

[DOI]

Vineet Rajani

Proceedings of the 31st IEEE Computer Security Foundations Symposium, 2018

2017

Type systems for information flow control: the question of granularity.

[BibT_eX]

[DOI]

ACM SIGLOG News, 2017

Robust and compositional verification of object capability patterns.

[BibT_eX]

[DOI]

David Swasey

Derek Dreyer

Proc. ACM Program. Lang., 2017

A relational logic for higher-order programs.

[BibT_eX]

[DOI]

Proc. ACM Program. Lang., 2017

Encrypting Messages for Incomplete Chains of Certificates.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2017

An Instrumenting Compiler for Enforcing Confidentiality in Low-Level Code.

[BibT_eX]

[DOI]

CoRR, 2017

Robust Hyperproperty Preservation for Secure Compilation (Extended Abstract).

[BibT_eX]

[DOI]

CoRR, 2017

Qapla: Policy compliance for database-backed systems.

[BibT_eX]

[DOI]

Proceedings of the 26th USENIX Security Symposium, 2017

Relational cost analysis.

[BibT_eX]

[DOI]

Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

WebPol: Fine-Grained Information Flow Policies for Web Browsers.

[BibT_eX]

[DOI]

Proceedings of the Computer Security - ESORICS 2017, 2017

Secure Compilation and Hyperproperty Preservation.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016

Thoth: Comprehensive Policy Compliance in Data Retrieval Systems.

[BibT_eX]

[DOI]

Eslam Elnikety

Aastha Mehta

Peter Druschel

Proceedings of the 25th USENIX Security Symposium, 2016

Asymmetric Secure Multi-execution with Declassification.

[BibT_eX]

[DOI]

Iulia Bolosteanu

Proceedings of the Principles of Security and Trust - 5th International Conference, 2016

Light-Weight Contexts: An OS Abstraction for Safety and Performance.

[BibT_eX]

[DOI]

James Litton

Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

A type theory for incremental computational complexity with control flow changes.

[BibT_eX]

[DOI]

Ezgi Çiçek

Zoe Paraskevopoulou

Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, 2016

Progress-Sensitive Security for SPARK.

[BibT_eX]

[DOI]

Willard Rafnsson

Andrei Sabelfeld

Proceedings of the Engineering Secure Software and Systems - 8th International Symposium, 2016

On Access Control, Capabilities, Their Equivalence, and Confused Deputy Attacks.

[BibT_eX]

[DOI]

Vineet Rajani

Tamara Rezk

Proceedings of the IEEE 29th Computer Security Foundations Symposium, 2016

Causally Consistent Dynamic Slicing.

[BibT_eX]

[DOI]

Roly Perera

James Cheney

Proceedings of the 27th International Conference on Concurrency Theory, 2016

2015

System M: A Program Logic for Code Sandboxing and Identification.

[BibT_eX]

[DOI]

CoRR, 2015

Guardat: enforcing data policies at the storage layer.

[BibT_eX]

[DOI]

Proceedings of the Tenth European Conference on Computer Systems, 2015

Refinement Types for Incremental Computational Complexity.

[BibT_eX]

[DOI]

Ezgi Çiçek

Umut A. Acar

Proceedings of the Programming Languages and Systems, 2015

Information Flow Control for Event Handling and the DOM in Web Browsers.

[BibT_eX]

[DOI]

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

A Logic of Programs with Interface-Confined Code.

[BibT_eX]

[DOI]

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

Program Actions as Actual Causes: A Building Block for Accountability.

[BibT_eX]

[DOI]

Proceedings of the IEEE 28th Computer Security Foundations Symposium, 2015

Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM SIGSAC Conference on Computer and Communications Security, 2015

2014

Information Flow Control in WebKit's JavaScript Bytecode.

[BibT_eX]

[DOI]

Proceedings of the Principles of Security and Trust - Third International Conference, 2014

Generalizing Permissive-Upgrade in Dynamic Information Flow Analysis.

[BibT_eX]

[DOI]

Proceedings of the Ninth Workshop on Programming Languages and Analysis for Security, 2014

Privacy-preserving audit for broker-based health information exchange.

[BibT_eX]

[DOI]

Proceedings of the Fourth ACM Conference on Data and Application Security and Privacy, 2014

Temporal Mode-Checking for Runtime Monitoring of Privacy Policies.

[BibT_eX]

[DOI]

Proceedings of the Computer Aided Verification - 26th International Conference, 2014

2013

Dependent Type Theory for Verification of Information Flow and Access Control Policies.

[BibT_eX]

[DOI]

Aleksandar Nanevski

Anindya Banerjee

ACM Trans. Program. Lang. Syst., 2013

2012

Stateful authorization logic - Proof theory and a case study.

[BibT_eX]

[DOI]

J. Comput. Secur., 2012

Labeled Goal-Directed Search in Access Control Logic.

[BibT_eX]

[DOI]

Daniele Rispoli

Proceedings of the Security and Trust Management - 8th International Workshop, 2012

Countermodels from Sequent Calculi in Multi-Modal Logics.

[BibT_eX]

[DOI]

Neelakantan R. Krishnaswami

Sara Negri

Proceedings of the 27th Annual IEEE Symposium on Logic in Computer Science, 2012

Superficially substructural types.

[BibT_eX]

[DOI]

Aaron Turon

Derek Dreyer

Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2012

Labeled Sequent Calculi for Access Control Logics: Countermodels, Saturation and Abduction.

[BibT_eX]

[DOI]

Daniele Rispoli

Proceedings of the 25th IEEE Computer Security Foundations Symposium, 2012

2011

On Adversary Models and Compositional Security.

[BibT_eX]

[DOI]

IEEE Secur. Priv., 2011

A Logical Method for Policy Enforcement over Evolving Audit Logs

[BibT_eX]

[DOI]

Limin Jia

Anupam Datta

CoRR, 2011

A Proof-Carrying File System with Revocable and Use-Once Certificates.

[BibT_eX]

[DOI]

Jamie Morgenstern

Proceedings of the Security and Trust Management - 7th International Workshop, 2011

New Modalities for Access Control Logics: Permission, Control and Ratification.

[BibT_eX]

[DOI]

Proceedings of the Security and Trust Management - 7th International Workshop, 2011

Verification of Information Flow and Access Control Policies with Dependent Types.

[BibT_eX]

[DOI]

Aleksandar Nanevski

Anindya Banerjee

Proceedings of the 32nd IEEE Symposium on Security and Privacy, 2011

Understanding and Protecting Privacy: Formal Semantics and Principled Audit Mechanisms.

[BibT_eX]

[DOI]

Proceedings of the Information Systems Security - 7th International Conference, 2011

Policy auditing over incomplete logs: theory, implementation and applications.

[BibT_eX]

[DOI]

Limin Jia

Anupam Datta

Proceedings of the 18th ACM Conference on Computer and Communications Security, 2011

2010

Compositional System Security with Interface-Confined Adversaries.

[BibT_eX]

[DOI]

Proceedings of the 26th Conference on the Mathematical Foundations of Programming Semantics, 2010

Experiences in the logical specification of the HIPAA and GLBA privacy laws.

[BibT_eX]

[DOI]

Proceedings of the 2010 ACM Workshop on Privacy in the Electronic Society, 2010

A Proof-Carrying File System.

[BibT_eX]

[DOI]

Proceedings of the 31st IEEE Symposium on Security and Privacy, 2010

2009

A Logic of Secure Systems and its Application to Trusted Computing.

[BibT_eX]

[DOI]

Proceedings of the 30th IEEE Symposium on Security and Privacy (SP 2009), 2009

PCAL: Language Support for Proof-Carrying Authorization Systems.

[BibT_eX]

[DOI]

Avik Chaudhuri

Proceedings of the Computer Security, 2009

2008

A Modal Deconstruction of Access Control Logics.

[BibT_eX]

[DOI]

Martín Abadi

Proceedings of the Foundations of Software Science and Computational Structures, 2008

An Authorization Logic With Explicit Time.

[BibT_eX]

[DOI]

Henry DeYoung

Proceedings of the 21st IEEE Computer Security Foundations Symposium, 2008

2007

Consumable Credentials in Linear-Logic-Based Access-Control Systems.

[BibT_eX]

[DOI]

Proceedings of the Network and Distributed System Security Symposium, 2007

2006

A Linear Logic of Authorization and Knowledge.

[BibT_eX]

[DOI]

Proceedings of the Computer Security, 2006

Non-Interference in Constructive Authorization Logic.

[BibT_eX]

[DOI]

Proceedings of the 19th IEEE Computer Security Foundations Workshop, 2006

2005

Type-Directed Concurrency.

[BibT_eX]

[DOI]

Proceedings of the CONCUR 2005 - Concurrency Theory, 16th International Conference, 2005

2004

Effective Chemistry for Synchrony and Asynchrony.

[BibT_eX]

[DOI]