Search Results

Documents authored by Wang, Chao

Document
DOI: 10.4230/LIPIcs.ECOOP.2026.4
Efficient Symbolic Execution of Software Under Fault Attacks

Authors: Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang

Published in: LIPIcs, Volume 372, 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing methods for analyzing the impact of maliciously injected hardware faults on the embedded software, they suffer from inaccurate fault modeling and inefficient fault analysis. To overcome these limitations, we propose two novel techniques. First, we propose a new fault modeling technique that leverages automated program transformation to add symbolic variables to the original program, to accurately model the new program behavior induced by the injected faults. This new fault modeling approach has two advantages over existing techniques: (a) the fault-induced program behavior is closely related to what attackers exploit in practice and (b) the automatically transformed program may be analyzed by any downstream fault analysis algorithm. Second, we propose an efficient symbolic execution algorithm that is designed specifically for conducting fault analysis on the transformed program. It leverages two pruning techniques to mitigate path explosion, which is the main performance bottleneck of symbolic execution in general and, in this particular application, is exacerbated by the additional fault-induced program behavior. We have implemented the proposed method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art techniques. Specifically, our method not only drastically reduces the overall running time of symbolic execution but also retains its error detection capabilities. Compared to the current state-of-the-art, it is able to detect previously-missed safety violations and at the same time avoid bogus violations. Furthermore, compared to the baseline algorithm, our optimized symbolic execution algorithm can be orders-of-magnitude faster.
Cite as

Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang. Efficient Symbolic Execution of Software Under Fault Attacks. In 40th European Conference on Object-Oriented Programming (ECOOP 2026). Leibniz International Proceedings in Informatics (LIPIcs), Volume 372, pp. 4:1-4:25, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@InProceedings{fang_et_al:LIPIcs.ECOOP.2026.4,
  author =	{Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
  title =	{{Efficient Symbolic Execution of Software Under Fault Attacks}},
  booktitle =	{40th European Conference on Object-Oriented Programming (ECOOP 2026)},
  pages =	{4:1--4:25},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-423-9},
  ISSN =	{1868-8969},
  year =	{2026},
  volume =	{372},
  editor =	{Krebbers, Robbert and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2026.4},
  URN =		{urn:nbn:de:0030-drops-261009},
  doi =		{10.4230/LIPIcs.ECOOP.2026.4},
  annote =	{Keywords: Symbolic Execution, Safety Verification, Fault Attack, Embedded Software}
}
Document
Artifact
DOI: 10.4230/DARTS.12.1.10
Efficient Symbolic Execution of Software under Fault Attacks (Artifact)

Authors: Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang

Published in: DARTS, Volume 12, Issue 1, Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026)

Abstract
We propose a symbolic execution method for analyzing the safety of software under fault attacks both accurately and efficiently. Fault attacks leverage physically injected hardware faults in an embedded system to break the safety of a software program. While there are existing methods for analyzing the impact of maliciously injected hardware faults on the embedded software, they suffer from inaccurate fault modeling and inefficient fault analysis. To overcome these limitations, we propose two novel techniques. First, we propose a new fault modeling technique that leverages automated program transformation to add symbolic variables to the original program, to accurately model the new program behavior induced by the injected faults. This new fault modeling approach has two advantages over existing techniques: (a) the fault-induced program behavior is closely related to what attackers exploit in practice and (b) the automatically transformed program may be analyzed by any downstream fault analysis algorithm. Second, we propose an efficient symbolic execution algorithm that is designed specifically for conducting fault analysis on the transformed program. It leverages two pruning techniques to mitigate path explosion, which is the main performance bottleneck of symbolic execution in general and, in this particular application, is exacerbated by the additional fault-induced program behavior. We have implemented the proposed method and evaluated it on a variety of benchmark programs. The experimental results show that our method significantly outperforms the state-of-the-art techniques. Specifically, our method not only drastically reduces the overall running time of symbolic execution but also retains its error detection capabilities. Compared to the current state-of-the-art, it is able to detect previously-missed safety violations and at the same time avoid bogus violations. Furthermore, compared to the baseline algorithm, our optimized symbolic execution algorithm can be orders-of-magnitude faster.
Cite as

Yuzhou Fang, Chenyu Zhou, Jingbo Wang, and Chao Wang. Efficient Symbolic Execution of Software under Fault Attacks (Artifact). In Special Issue of the 40th European Conference on Object-Oriented Programming (ECOOP 2026). Dagstuhl Artifacts Series (DARTS), Volume 12, Issue 1, pp. 10:1-10:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2026)

Copy BibTex To Clipboard

@Article{fang_et_al:DARTS.12.1.10,
  author =	{Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
  title =	{{Efficient Symbolic Execution of Software under Fault Attacks (Artifact)}},
  pages =	{10:1--10:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2026},
  volume =	{12},
  number =	{1},
  editor =	{Fang, Yuzhou and Zhou, Chenyu and Wang, Jingbo and Wang, Chao},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.12.1.10},
  URN =		{urn:nbn:de:0030-drops-261477},
  doi =		{10.4230/DARTS.12.1.10},
  annote =	{Keywords: Symbolic Execution, Safety Verification, Fault Attack, Embedded Software}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2025.22
Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions

Authors: Jacqueline L. Mitchell and Chao Wang

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
We propose an improved abstract interpretation based method for quantifying cache side-channel leakage by addressing two key components of precision loss in existing set-based cache abstractions. Our method targets two key sources of imprecision: (1) imprecision in the abstract transfer function used to update the abstract cache state when interpreting a memory access and (2) imprecision due to the incompleteness of the set-based domain. At the center of our method are two key improvements: (1) the introduction of a new transfer function for updating the abstract cache state which carefully leverages information in the abstract state to prevent the spurious aging of memory blocks and (2) a refinement of the set-based domain based on the finite powerset construction. We show that both the new abstract transformer and the domain refinement enjoy certain enhanced precision properties. We have implemented the method and compared it against the state-of-the-art technique on a suite of benchmark programs implementing both sorting algorithms and cryptographic algorithms. The experimental results show that our method is effective in improving the precision of cache side-channel leakage quantification.
Cite as

Jacqueline L. Mitchell and Chao Wang. Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 22:1-22:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{mitchell_et_al:LIPIcs.ECOOP.2025.22,
  author =	{Mitchell, Jacqueline L. and Wang, Chao},
  title =	{{Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{22:1--22:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.22},
  URN =		{urn:nbn:de:0030-drops-233140},
  doi =		{10.4230/LIPIcs.ECOOP.2025.22},
  annote =	{Keywords: Abstract interpretation, side-channel, leakage quantification, cache}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.18
Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact)

Authors: Jacqueline L. Mitchell and Chao Wang

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
This is the accompanying artifact for the ECOOP 25' paper "Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions".
Cite as

Jacqueline L. Mitchell and Chao Wang. Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 18:1-18:4, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{mitchell_et_al:DARTS.11.2.18,
  author =	{Mitchell, Jacqueline L. and Wang, Chao},
  title =	{{Quantifying Cache Side-Channel Leakage by Refining Set-Based Abstractions (Artifact)}},
  pages =	{18:1--18:4},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Mitchell, Jacqueline L. and Wang, Chao},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.18},
  URN =		{urn:nbn:de:0030-drops-233619},
  doi =		{10.4230/DARTS.11.2.18},
  annote =	{Keywords: Abstract interpretation, side-channel, leakage quantification, cache}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2023.16
Constraint Based Compiler Optimization for Energy Harvesting Applications

Authors: Yannan Li and Chao Wang

Published in: LIPIcs, Volume 263, 37th European Conference on Object-Oriented Programming (ECOOP 2023)

Abstract
We propose a method for optimizing the energy efficiency of software code running on small computing devices in the Internet of Things (IoT) that are powered exclusively by electricity harvested from ambient energy in the environment. Due to the weak and unstable nature of the energy source, it is challenging for developers to manually optimize the software code to deal with mismatch between the intermittent power supply and the computation demand. Our method overcomes the challenge by using a combination of three techniques. First, we use static program analysis to automatically identify opportunities for precomputation, i.e., computation that may be performed ahead of time as opposed to just in time. Second, we optimize the precomputation policy, i.e., a way to split and reorder steps of a computation task in the original software to match the intermittent power supply while satisfying a variety of system requirements; this is accomplished by formulating energy optimization as a constraint satisfiability problem and then solving the problem using an off-the-shelf SMT solver. Third, we use a state-of-the-art compiler platform (LLVM) to automate the program transformation to ensure that the optimized software code is correct by construction. We have evaluated our method on a large number of benchmark programs, which are C programs implementing secure communication protocols that are popular for energy-harvesting IoT devices. Our experimental results show that the method is efficient in optimizing all benchmark programs. Furthermore, the optimized programs significantly outperform the original programs in terms of energy efficiency and latency, and the overall improvement ranges from 2.3X to 36.7X.
Cite as

Yannan Li and Chao Wang. Constraint Based Compiler Optimization for Energy Harvesting Applications. In 37th European Conference on Object-Oriented Programming (ECOOP 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 263, pp. 16:1-16:29, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)

Copy BibTex To Clipboard

@InProceedings{li_et_al:LIPIcs.ECOOP.2023.16,
  author =	{Li, Yannan and Wang, Chao},
  title =	{{Constraint Based Compiler Optimization for Energy Harvesting Applications}},
  booktitle =	{37th European Conference on Object-Oriented Programming (ECOOP 2023)},
  pages =	{16:1--16:29},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-281-5},
  ISSN =	{1868-8969},
  year =	{2023},
  volume =	{263},
  editor =	{Ali, Karim and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2023.16},
  URN =		{urn:nbn:de:0030-drops-182096},
  doi =		{10.4230/LIPIcs.ECOOP.2023.16},
  annote =	{Keywords: Compiler, energy optimization, constraint solving, cryptography, IoT}
}
Document
DOI: 10.4230/LIPIcs.CONCUR.2017.16
Checking Linearizability of Concurrent Priority Queues

Authors: Ahmed Bouajjani, Constantin Enea, and Chao Wang

Published in: LIPIcs, Volume 85, 28th International Conference on Concurrency Theory (CONCUR 2017)

Abstract
Efficient implementations of concurrent objects such as atomic collections are essential to modern computing. Unfortunately their correctness criteria — linearizability with respect to given ADT specifications — are hard to verify. Verifying linearizability is undecidable in general, even on classes of implementations where the usual control-state reachability is decidable. In this work we consider concurrent priority queues which are fundamental to many multi-threaded applications like task scheduling or discrete event simulation, and show that verifying linearizability of such implementations is reducible to control-state reachability. This reduction entails the first decidability results for verifying concurrent priority queues with an unbounded number of threads, and it enables the application of existing safety-verification tools for establishing their correctness.
Cite as

Ahmed Bouajjani, Constantin Enea, and Chao Wang. Checking Linearizability of Concurrent Priority Queues. In 28th International Conference on Concurrency Theory (CONCUR 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 85, pp. 16:1-16:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{bouajjani_et_al:LIPIcs.CONCUR.2017.16,
  author =	{Bouajjani, Ahmed and Enea, Constantin and Wang, Chao},
  title =	{{Checking Linearizability of Concurrent Priority Queues}},
  booktitle =	{28th International Conference on Concurrency Theory (CONCUR 2017)},
  pages =	{16:1--16:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-048-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{85},
  editor =	{Meyer, Roland and Nestmann, Uwe},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2017.16},
  URN =		{urn:nbn:de:0030-drops-78079},
  doi =		{10.4230/LIPIcs.CONCUR.2017.16},
  annote =	{Keywords: Concurrency, Linearizability, Model Checking}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact