Skip to main content

Danfeng Zhang

Associate Professor of Computer Science
Computer Science
308 Research Drive Box 90129, Durham, NC 27704

Selected Publications


CtChecker: A Precise, Sound and Efficient Static Analysis for Constant-Time Programming

Conference Leibniz International Proceedings in Informatics, LIPIcs · September 1, 2024 Timing channel attacks are emerging as real-world threats to computer security. In cryptographic systems, an effective countermeasure against timing attacks is the constant-time programming discipline. However, strictly enforcing the discipline manually is ... Full text Cite

RECONSTRUCTION ATTACKS ON AGGRESSIVE RELAXATIONS OF DIFFERENTIAL PRIVACY

Journal Article Journal of Privacy and Confidentiality · August 27, 2024 Differential privacy is a widely accepted formal privacy definition that allows aggregate information about a dataset to be released while controlling privacy leakage for individuals whose records appear in the data. Due to the unavoidable tension between ... Full text Cite

EXACT PRIVACY ANALYSIS OF THE GAUSSIAN SPARSE HISTOGRAM MECHANISM

Journal Article Journal of Privacy and Confidentiality · January 1, 2024 Sparse histogram methods can be useful for returning differentially private counts of items in large or infinite histograms or large group-by queries, and more generally, releasing a set of statistics with sufficient item counts. We consider the Gaussian v ... Full text Cite

Hardware Support for Constant-Time Programming

Conference Proceedings of the 56th Annual IEEE/ACM International Symposium on Microarchitecture, MICRO 2023 · October 28, 2023 Side-channel attacks are one of the rising security concerns in modern computing platforms. Observing this, researchers have proposed both hardware-based and software-based strategies to mitigate side-channel attacks, targeting not only on-chip caches but ... Full text Cite

Quantifying and Mitigating Cache Side Channel Leakage with Differential Set

Journal Article Proceedings of the ACM on Programming Languages · October 16, 2023 Cache side-channel attacks leverage secret-dependent footprints in CPU cache to steal confidential information, such as encryption keys. Due to the lack of a proper abstraction for reasoning about cache side channels, existing static program analysis tools ... Full text Cite

Answering Private Linear Queries Adaptively using the Common Mechanism

Journal Article Proceedings of the VLDB Endowment · January 1, 2023 When analyzing confidential data through a privacy filter, a data scientist often needs to decide which queries will best support their intended analysis. For example, an analyst may wish to study noisy two-way marginals in a dataset produced by a mechanis ... Full text Cite

Free gap estimates from the exponential mechanism, sparse vector, noisy max and related algorithms

Journal Article VLDB Journal · January 1, 2023 Private selection algorithms, such as the exponential mechanism, noisy max and sparse vector, are used to select items (such as queries with large answers) from a set of candidates, while controlling privacy leakage in the underlying data. Such algorithms ... Full text Cite

An Optimal and Scalable Matrix Mechanism for Noisy Marginals under Convex Loss Functions

Conference Advances in Neural Information Processing Systems · January 1, 2023 Noisy marginals are a common form of confidentiality-protecting data release and are useful for many downstream tasks such as contingency table analysis, construction of Bayesian networks, and even synthetic data generation. Privacy mechanisms that provide ... Cite

Performant Binary Fuzzing without Source Code using Static Instrumentation

Conference 2022 IEEE Conference on Communications and Network Security, CNS 2022 · January 1, 2022 Advancements in fuzz testing have achieved the ability to quickly and comprehensively find security-critical faults in software systems. Yet, some of these techniques rely on access to source code, which is often unavailable in practice. In this paper, we ... Full text Cite

Towards a General-Purpose Dynamic Information Flow Policy

Conference Proceedings - IEEE Computer Security Foundations Symposium · January 1, 2022 Noninterference offers a rigorous end-to-end guarantee for secure propagation of information. However, real-world systems almost always involve security requirements that change during program execution, making noninterference inapplicable. Prior works all ... Full text Cite

DPGen: Automated Program Synthesis for Differential Privacy

Conference Proceedings of the ACM Conference on Computer and Communications Security · November 12, 2021 Differential privacy has become a de facto standard for releasing data in a privacy-preserving way. Creating a differentially private algorithm is a process that often starts with a noise-free (non-private) algorithm. The designer then decides where to add ... Full text Cite

SpecSafe: Detecting cache side channels in a speculative world

Journal Article Proceedings of the ACM on Programming Languages · October 1, 2021 The high-profile Spectre attack and its variants have revealed that speculative execution may leave secret-dependent footprints in the cache, allowing an attacker to learn confidential data. However, existing static side-channel detectors either ignore spe ... Full text Cite

Fluid: A framework for approximate concurrency via controlled dependency relaxation

Conference Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · June 18, 2021 In this work, we introduce the Fluid framework, a set of language, compiler and runtime extensions that allow for the expression of regions within which dataflow dependencies can be approximated in a disciplined manner. Our framework allows the eager execu ... Full text Cite

Ghost Thread: Effective User-Space Cache Side Channel Protection

Conference CODASPY 2021 - Proceedings of the 11th ACM Conference on Data and Application Security and Privacy · April 26, 2021 Cache-based side channel attacks pose a serious threat to computer security. Numerous cache attacks have been demonstrated, highlighting the need for effective and efficient defense mechanisms to shield systems from this threat. In this paper, we propose a ... Full text Cite

Optimizing fitness-for-use of differentially private linear Queries

Journal Article Proceedings of the VLDB Endowment · January 1, 2021 In practice, differentially private data releases are designed to support a variety of applications. A data release is fit for use if it meets target accuracy requirements for each application. In this paper, we consider the problem of answering linear que ... Full text Cite

CheckDP: An Automated and Integrated Approach for Proving Differential Privacy or Finding Precise Counterexamples

Conference Proceedings of the ACM Conference on Computer and Communications Security · October 30, 2020 We propose CheckDP, an automated and integrated approach for proving or disproving claims that a mechanism is differentially private. CheckDP can find counterexamples for mechanisms with subtle bugs for which prior counterexample generators have failed. Fu ... Full text Cite

BCoal: Bucketing-based memory coalescing for efficient and secure GPUs

Conference Proceedings - 2020 IEEE International Symposium on High Performance Computer Architecture, HPCA 2020 · February 1, 2020 Graphics Processing Units (GPUs) are becoming a de facto choice for accelerating applications from a wide range of domains ranging from graphics to high-performance computing. As a result, it is getting increasingly desirable to improve the cooperation bet ... Full text Cite

Free gap information from the differentially private sparse vector and noisy max mechanisms

Conference Proceedings of the VLDB Endowment · January 1, 2020 Noisy Max and Sparse Vector are selection algorithms for differential privacy and serve as building blocks for more complex algorithms. In this paper we show that both algorithms can release additional information for free (i.e., at no additional privacy c ... Full text Cite

Proving differential privacy with shadow execution

Conference Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · June 8, 2019 Recent work on formal verification of differential privacy shows a trend toward usability and expressiveness - generating a correctness proof of sophisticated algorithm while minimizing the annotation burden on programmers. Sometimes, combining those two r ... Full text Cite

CaSym: Cache aware symbolic execution for side channel detection and mitigation

Conference Proceedings - IEEE Symposium on Security and Privacy · May 1, 2019 Cache-based side channels are becoming an important attack vector through which secret information can be leaked to malicious parties. implementations and Previous work on cache-based side channel detection, however, suffers from the code coverage problem ... Full text Cite

Identifying cache-based side channels through secret-augmented abstract interpretation

Conference Proceedings of the 28th USENIX Security Symposium · January 1, 2019 Cache-based side channels enable a dedicated attacker to reveal program secrets by measuring the cache access patterns. Practical attacks have been shown against real-world crypto algorithm implementations such as RSA, AES, and ElGamal. By far, identifying ... Cite

A derivation framework for dependent security label inference

Journal Article Proceedings of the ACM on Programming Languages · November 1, 2018 Dependent security labels (security labels that depend on program states) in various forms have been introduced to express rich information flow policies. They are shown to be essential in the verification of real-world software and hardware systems such a ... Cite

Detecting violations of differential privacy

Conference Proceedings of the ACM Conference on Computer and Communications Security · October 15, 2018 The widespread acceptance of differential privacy has led to the publication of many sophisticated algorithms for protecting privacy. However, due to the subtle nature of this privacy definition, many such algorithms have bugs that make them violate their ... Full text Cite

RCoal: Mitigating GPU Timing Attack via Subwarp-Based Randomized Coalescing Techniques

Conference Proceedings - International Symposium on High-Performance Computer Architecture · March 27, 2018 Graphics processing units (GPUs) are becoming default accelerators in many domains such as high-performance computing (HPC), deep learning, and virtual/augmented reality. Recently, GPUs have also shown significant speedups for a variety of security-sensiti ... Full text Cite

Towards a Flow- and Path-Sensitive Information Flow Analysis

Conference Proceedings - IEEE Computer Security Foundations Symposium · September 25, 2017 This paper investigates a flow- and path-sensitive static information flow analysis. Compared with security type systems with fixed labels, it has been shown that flow-sensitive type systems accept more secure programs. We show that an information flow ana ... Full text Cite

SHErrLoc: A static holistic error locator

Journal Article ACM Transactions on Programming Languages and Systems · August 1, 2017 We introduce a general way to locate programmer mistakes that are detected by static analyses. The program analysis is expressed in a general constraint language that is powerful enough to model type checking, information flow analysis, dataflow analysis, ... Full text Cite

Verification of a Practical Hardware Security Architecture Through Static Information Flow Analysis

Conference ACM SIGPLAN Notices · May 12, 2017 Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify importa ... Full text Cite

LightDP: towards automating differential privacy proofs

Conference ACM SIGPLAN Notices · May 11, 2017 The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomeno ... Full text Cite

Verification of a practical Hardware security architecture through static information flow analysis

Conference International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS · April 4, 2017 Hardware-based mechanisms for software isolation are becoming increasingly popular, but implementing these mechanisms correctly has proved difficult, undermining the root of security. This work introduces an effective way to formally verify important prope ... Full text Cite

Cached: Identifying cache-based timing channels in production software

Conference Proceedings of the 26th USENIX Security Symposium · January 1, 2017 Side-channel attacks recover secret information by analyzing the physical implementation of cryptosystems based on non-functional computational characteristics, e.g. time, power, and memory usage. Among all well-known side channels, cache-based timing chan ... Cite

LightDP: Towards automating differential privacy proofs

Conference Conference Record of the Annual ACM Symposium on Principles of Programming Languages · January 1, 2017 The growing popularity and adoption of differential privacy in academic and industrial settings has resulted in the development of increasingly sophisticated algorithms for releasing information while preserving privacy. Accompanying this phenomenon is the ... Full text Cite

SecDCP: Secure dynamic cache partitioning for efficient timing channel protection

Conference Proceedings - Design Automation Conference · June 5, 2016 In today's multicore processors, the last-level cache is often shared by multiple concurrently running processes to make efficient use of hardware resources. However, previous studies have shown that a shared cache is vulnerable to timing channel attacks t ... Full text Cite

Lattice priority scheduling: Low-overhead timing-channel protection for a shared memory controller

Conference Proceedings - International Symposium on High-Performance Computer Architecture · April 1, 2016 Computer hardware is increasingly shared by distrusting parties in platforms such as commercial clouds and web servers. Though hardware sharing is critical for performance and efficiency, this sharing creates timing-channel vulnerabilities in hardware comp ... Full text Cite

Diagnosing type errors with class

Conference ACM SIGPLAN Notices · June 1, 2015 Type inference engines often give terrible error messages, and the more sophisticated the type system the worse the problem. We show that even with the highly expressive type system implemented by the Glasgow Haskell Compiler (GHC)-including type classes, ... Full text Cite

A hardware design language for timing-sensitive information-flow security

Conference International Conference on Architectural Support for Programming Languages and Operating Systems - ASPLOS · March 14, 2015 Information security can be compromised by leakage via low-level hardware features. One recently prominent example is cache probing attacks, which rely on timing channels created by caches. We introduce a hardware design language, SecVerilog, which makes i ... Full text Cite

Toward general diagnosis of static errors

Conference Conference Record of the Annual ACM Symposium on Principles of Programming Languages · February 11, 2014 We introduce a general way to locate programmer mistakes that are detected by static analyses such as type checking. The program analysis is expressed in a constraint language in which mistakes result in unsatisfiable constraints. Given an unsatisfiable sy ... Full text Cite

Ironclad apps: End-to-end security via automated full-system verification

Conference Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2014 · January 1, 2014 An Ironclad App lets a user securely transmit her data to a remote machine with the guarantee that every instruction executed on that machine adheres to a formal abstract specification of the app's behavior. This does more than eliminate implementation vul ... Cite

Language-based control and mitigation of timing channels

Conference ACM SIGPLAN Notices · August 1, 2012 We propose a new language-based approach to mitigating timing channels. In this language, well-Typed programs provably leak only a bounded amount of information over time through external timing channels. By incorporating mechanisms for predictive mitigati ... Full text Cite

Language-based control and mitigation of timing channels

Conference Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI) · July 9, 2012 We propose a new language-based approach to mitigating timing channels. In this language, well-typed programs provably leak only a bounded amount of information over time through external timing channels. By incorporating mechanisms for predictive mitigati ... Full text Cite

Predictive mitigation of timing channels in interactive systems

Conference Proceedings of the ACM Conference on Computer and Communications Security · November 14, 2011 Timing channels remain a difficult and important problem for information security. Recent work introduced predictive mitigation, a new way to mitigating leakage through timing channels; this mechanism works by predicting timing from past behavior, and then ... Full text Cite

Predictive black-box mitigation of timing channels

Conference Proceedings of the ACM Conference on Computer and Communications Security · December 16, 2010 We investigate techniques for general black-box mitigation of timing channels. The source of events is wrapped by a timing mitigator that delays output events so that they contain only a bounded amount of information. We introduce a general class of timing ... Full text Cite

Automated aspect recommendation through clustering-based fan-in analysis

Conference ASE 2008 - 23rd IEEE/ACM International Conference on Automated Software Engineering, Proceedings · November 21, 2008 Identifying code implementing a crosscutting concern (CCC) automatically can benefit the maintainability and evolvability of the application. Although many approaches have been proposed to identify potential aspects, a lot of manual work is typically requi ... Full text Cite

AspectC2C: A symmetric aspect extension to the C language

Journal Article ACM SIGPLAN Notices · February 1, 2008 By separating crosscutting concerns into modules, aspect-oriented programming (AOP) can greatly improve the maintainability, understandability and reusability of software. However, the asymmetric paradigm adopted by most AOP extensions could bring crosscut ... Cite

Toward Efficient Aspect Mining for Linux

Conference 14th Asia-Pacific Software Engineering Conference (APSEC'07) · December 2007 Full text Cite

Toward efficient aspect mining for linux

Conference Proceedings - Asia-Pacific Software Engineering Conference, APSEC · December 1, 2007 Code implementing a crosscutting concern spreads over many parts of the Linux code. Identifying these code automatically can benefit both the maintainability and evolvability of Linux. In this paper, we present a case study on how to identify aspects in th ... Full text Cite