Attack Synthesis for Strings using Meta-Heuristics

Ismet Burak Kadron; Lucas Bang; Seemanta Saha; Tevfik Bultan; William Eiers

arxiv: 1907.11710 · v1 · pith:JIXZ6UYZnew · submitted 2019-07-26 · 💻 cs.SE · cs.CR

Attack Synthesis for Strings using Meta-Heuristics

Seemanta Saha , Ismet Burak Kadron , William Eiers , Lucas Bang , Tevfik Bultan This is my paper

Pith reviewed 2026-05-24 15:37 UTC · model grok-4.3

classification 💻 cs.SE cs.CR

keywords side channel attacksattack synthesistiming attacksstring processingmetaheuristicsmodel countingsymbolic executionentropy

0 comments

The pith

Meta-heuristic search synthesizes adaptive attacks that recover secret strings from timing side-channels in string-manipulating code.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

This paper develops automated techniques for creating side-channel attacks that extract secret string values by measuring execution times of programs that process those strings. The approach extracts path constraints through symbolic execution, estimates probabilities of different execution paths using automata-based model counting, and applies meta-heuristic methods to select inputs that maximize the entropy reduction about the secret. A sympathetic reader would care because it turns manual attack crafting into an algorithmic process that could expose vulnerabilities in string-handling software. The synthesis is iterative, building on previous observations to choose the next input.

Core claim

The paper claims that by using meta-heuristics to maximize information gain based on entropy estimates from automata model counting on path constraints obtained via symbolic execution, it is possible to synthesize sequences of inputs that, when executed on string-manipulating code, reveal enough timing-based partial information to recover the full secret string at the end of the attack.

What carries the argument

The meta-heuristic optimization loop that selects inputs to maximize expected information gain, guided by probability estimates from automata-based model counting.

If this is right

Full secret recovery becomes possible through a series of adaptive timing observations.
Attack generation is automated for string-based secrets.
The method applies to code with string manipulation operations that have variable timing.
Information gain is quantified using entropy to guide the search.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar techniques might apply to synthesizing attacks on other data types if model counting can be adapted.
The approach could be used defensively to test software for timing leaks.
Limitations in model counting accuracy would directly affect attack success rates.

Load-bearing premise

The meta-heuristic search will find inputs that provide enough information gain in each step to eventually allow complete recovery of the secret.

What would settle it

A test where the attack synthesis is run against a string-manipulating function with a fixed secret, and the final reconstructed secret does not match the original after a bounded number of steps.

Figures

Figures reproduced from arXiv: 1907.11710 by Ismet Burak Kadron, Lucas Bang, Seemanta Saha, Tevfik Bultan, William Eiers.

**Figure 1.** Figure 1: PIN checking example. ing, and genetic algorithms; and (3) we present attack synthesis techniques based on automata-based model counting. A Motivating Example. Consider a PIN-based authentication function ( [PITH_FULL_IMAGE:figures/full_fig_p001_1.png] view at source ↗

read the original abstract

Information leaks are a significant problem in modern computer systems and string manipulation is prevalent in modern software. We present techniques for automated synthesis of side-channel attacks that recover secret string values based on timing observations on string manipulating code. Our attack synthesis techniques iteratively generate inputs which, when fed to code that accesses the secret, reveal partial information about the secret based on the timing observations, leading to recovery of the secret at the end of the attack sequence. We use symbolic execution to extract path constraints, automata-based model counting to estimate the probability of execution paths, and meta-heuristic methods to maximize information gain based on entropy for synthesizing adaptive attack steps.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

The paper sketches an iterative synthesis loop for timing attacks on string secrets but the abstract supplies no results to check if it recovers anything.

read the letter

The main takeaway is a pipeline that turns symbolic execution, automata model counting, and meta-heuristic search into an adaptive generator for timing-based string attacks. Each step picks an input meant to maximize expected information gain on the secret until the observations isolate it. That loop is the concrete new piece; prior work had the separate components but not this closed synthesis process for attack generation. The description is clear on how the pieces fit together and why entropy is the right objective for choosing the next input. The construction itself looks internally consistent: path constraints feed the counting step, probabilities feed the search, and the loop stops when the secret is pinned down. No obvious mismatch between the timing model and the constraints appears in the framing. The soft spot is the total absence of any data. The abstract gives the intended method but zero success rates, runtimes, or comparisons against random inputs or simpler heuristics. Without that, the claim that the meta-heuristics will reliably produce enough gain to recover the full secret stays untested. The assumption that model-counting estimates will be accurate enough in practice and that timing observations will be clean enough to drive the loop could still break. This is for people working on automated security testing and side-channel analysis who want a way to generate leak-revealing inputs rather than just detect leaks after the fact. It deserves a serious referee because the problem is real, the pipeline is specified at a usable level, and the components are established; the evaluation is the obvious missing piece that referees can ask for.

Referee Report

2 major / 1 minor

Summary. The paper claims to present automated techniques for synthesizing adaptive side-channel attacks that recover secret string values from timing observations on string-manipulating code. The approach iteratively generates inputs by extracting path constraints via symbolic execution, estimating path probabilities with automata-based model counting, and using meta-heuristic search to maximize entropy-based information gain, continuing until the secret is isolated.

Significance. If the synthesis loop proves effective in practice, the work would contribute a systematic, search-based method for generating timing attacks on common string operations, potentially aiding both vulnerability discovery and automated security testing. The combination of symbolic execution, model counting, and entropy-guided meta-heuristics represents a coherent integration of existing techniques for information-gain-driven attack synthesis.

major comments (2)

[Abstract] Abstract: The central claim that the iterative synthesis produces inputs leading to full secret recovery is presented without any experimental results, success rates, case studies, or comparison data, making it impossible to assess whether the meta-heuristic entropy maximization actually yields sufficient information gain in practice.
[Synthesis loop description] Synthesis loop description (paragraph on the attack sequence): The assumption that meta-heuristic search guided by automata-based entropy estimates will reliably isolate the secret is stated at a high level but lacks any concrete bounds, termination arguments, or example derivations showing how partial timing observations accumulate to full recovery.

minor comments (1)

The description of how timing observations translate into path constraints could be clarified with an explicit small example showing the mapping from observation to updated secret distribution.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the constructive feedback on our manuscript describing attack synthesis for strings. We address each major comment below.

read point-by-point responses

Referee: [Abstract] Abstract: The central claim that the iterative synthesis produces inputs leading to full secret recovery is presented without any experimental results, success rates, case studies, or comparison data, making it impossible to assess whether the meta-heuristic entropy maximization actually yields sufficient information gain in practice.

Authors: The abstract summarizes the proposed synthesis technique at a high level. The full manuscript contains an experimental evaluation section with case studies on common string operations (e.g., strcmp) and reports on success rates for secret recovery. To improve clarity for readers, we will revise the abstract to include a concise reference to these empirical results and key findings on information gain. revision: yes
Referee: [Synthesis loop description] Synthesis loop description (paragraph on the attack sequence): The assumption that meta-heuristic search guided by automata-based entropy estimates will reliably isolate the secret is stated at a high level but lacks any concrete bounds, termination arguments, or example derivations showing how partial timing observations accumulate to full recovery.

Authors: We agree the description of the synthesis loop is high-level. The loop is intended to terminate when remaining entropy reaches zero (i.e., a single secret remains), which follows from the finite secret space and the fact that each adaptive observation is chosen to maximize information gain. We will add an explicit termination argument, concrete bounds based on the model-counting estimates, and a worked example derivation in the revised manuscript. revision: yes

Circularity Check

0 steps flagged

No significant circularity in derivation chain

full rationale

The paper describes an algorithmic synthesis technique that combines symbolic execution for path constraints, automata-based model counting for probability estimates, and meta-heuristic search to maximize entropy-based information gain in an iterative loop. No equations, fitted parameters, or first-principles derivations are presented that reduce any claimed prediction or result to the inputs by construction. The central claim is a practical method for generating adaptive attack sequences rather than a mathematical equivalence or uniqueness theorem, and no load-bearing self-citations or ansatzes imported via prior work are evident in the provided description.

Axiom & Free-Parameter Ledger

0 free parameters · 0 axioms · 0 invented entities

Abstract-only review; no explicit free parameters, axioms, or invented entities are stated in the provided text.

pith-pipeline@v0.9.0 · 5638 in / 1090 out tokens · 16931 ms · 2026-05-24T15:37:36.317833+00:00 · methodology

discussion (0)

Reference graph

Works this paper leans on

26 extracted references · 26 canonical work pages

[1]

8299” 63 15 5.906 “1392

INTRODUCTION Modern software systems store and manipulate sensitive inf orma- tion. It is crucial for software developers to write code in a man- ner that prevents disclosure of sensitive information to ar bitrary users. However, computation that accesses sensitive infor mation can have attacker-measurable characteristics that leaks i nforma- tion. This c...

work page 1950
[2]

We consider functions F that take as input a secret string h∈ H and an attacker-controlled string l∈ L and that have side-channel observations o∈ O

AUTOMATIC ATTACK SYNTHESIS In this section we give a two phase approach that synthesizes attacks (Procedure 1). We consider functions F that take as input a secret string h∈ H and an attacker-controlled string l∈ L and that have side-channel observations o∈ O. Procedure 1 SynthesizeAttack(F (h, l), Ch, h∗ ) This procedure calls the GenerateConstraints and...

work page
[3]

In the following discussion, H, L, and O are random variables repre- senting high-security input, low-security input, and side -channel observation respectively

ENTROPY-BASED OBJECTIVE FUNCTION Here we derive an objective function to measure the amount of in- formation an attacker expects to gain by choosing an input va lue lval to be used in the attack search heuristics of Section 4. In the following discussion, H, L, and O are random variables repre- senting high-security input, low-security input, and side -ch...

work page
[4]

temperature

ATTACK SYNTHESIS HEURISTICS At every attack step the goal is to choose a low input l∗ that re- veals information about h∗ . Here we describe diﬀerent techniques for synthesizing attack inputs l∗ . Each approach uses a diﬀerent heuristic to explore a subset of the possible low inputs. To s earch the input space eﬃciently, we ﬁrst observe that we need to re...

work page
[5]

We implemented Procedure 2 using Symbolic Path Finder (SPF) [16]

IMPLEMENTATIONS AND EXPERIMENTS Implementation. We implemented Procedure 2 using Symbolic Path Finder (SPF) [16]. We implemented Procedure 3 as a Java program that takes the observation constraints generated b y Pro- cedure 2 as input, along with Ch and h∗ . The variations of At- tackInput from Section 4 (Procedures 4, 5, and 6) are imple- mented in Java....

work page
[6]

We present the mean values of the results in Tables 4

We ran each experiment for 5 randomly chosen secrets. We present the mean values of the results in Tables 4. For RA, we s et the sample size K to 20. For SA, we set the temperature range ( t to tmin) from 10 to 0.001 and cooling rate k as 0.1. For GA, we set population size popSize to 20, oﬀspring size as 10, number of best selections N as 10. Results. In...

work page
[7]

There has been recent results on synthesizing attacks or qua nti- fying information leakage under a model where the attacker c an make multiple runs of the system [2, 3, 6, 12, 15]

RELATED WORK There has been prior work on analyzing side-channels [2, 4, 5 , 15]. There has been recent results on synthesizing attacks or qua nti- fying information leakage under a model where the attacker c an make multiple runs of the system [2, 3, 6, 12, 15]. For example , LeakWatch [6] estimates leakage in Java programs based on sa m- pling program e...

work page
[8]

CONCLUSION In this paper we presented techniques for synthesizing adap tive attacks for string manipulating programs. To the best of our knowledge this is the ﬁrst work which is able to automaticall y dis- cover side channel vulnerabilities by synthesizing attacks targeting string manipulating functions. We presented several heuri stics for attack synthes...

work page
[9]

Automata-based model counting for string constraints

Abdulbaki Aydin, Lucas Bang, and Tevﬁk Bultan. Automata-based model counting for string constraints. In Proceedings of the 27th International Conference on Computer Aided Veriﬁcation (CA V), pages 255–272, 2015

work page 2015
[10]

Pasareanu, and Tevﬁk Bultan

Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevﬁk Bultan. String analysis for side channels with segmented oracles. In Proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering , 2016

work page 2016
[11]

Online synthesis of adaptive side-channel attacks based on noisy observations

Lucas Bang, Nicolas Rosner, and Tevﬁk Bultan. Online synthesis of adaptive side-channel attacks based on noisy observations. In Proceedings of the IEEE European Symposium on Security and Privacy (EuroS&P) , 2018

work page 2018
[12]

Remote Timing Attacks Are Practical

David Brumley and Dan Boneh. Remote Timing Attacks Are Practical. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12 , SSYM’03, pages 1–1, Berkeley, CA, USA, 2003. USENIX Association

work page 2003
[13]

Side-channel leaks in web applications: A reality today, a challenge tomorrow

Shuo Chen, Rui Wang, XiaoFeng Wang, and Kehuan Zhang. Side-channel leaks in web applications: A reality today, a challenge tomorrow. In Proceedings of the 2010 IEEE Symposium on Security and Privacy , SP ’10, pages 191–206, Washington, DC, USA, 2010. IEEE Computer Society

work page 2010
[14]

Leakwatch: Estimating information leakage from java programs

Tom Chothia, Yusuke Kawamoto, and Chris Novakovic. Leakwatch: Estimating information leakage from java programs. In Computer Security - ESORICS 2014 - 19th European Symposium on Research in Computer Security, Wroclaw, Poland, September 7-11, 2014. Proceedings, Part II, pages 219–236, 2014

work page 2014
[15]

Cover and Joy A

Thomas M. Cover and Joy A. Thomas. Elements of Information Theory (Wiley Series in Telecommunications and Signal Processing) . Wiley-Interscience, 2006

work page 2006
[16]

Time trial: Racing towards practical remote timing attacks

Joel Sandin Daniel Mayer. Time trial: Racing towards practical remote timing attacks. https://www.nccgroup.trust/globalassets/our-research/us/whitepapers/TimeTrial.pdf, 2014

work page 2014
[17]

Genetic algorithms in search, optimization, and machine learning

David E Goldberg. Genetic algorithms in search, optimization, and machine learning. Technical report, 198 9

work page
[18]

James C. King. Symbolic execution and program testing. Commun. ACM , 19(7):385–394, July 1976

work page 1976
[19]

Optimization by simulated annealing

Scott Kirkpatrick, C Daniel Gelatt, and Mario P Vecchi. Optimization by simulated annealing. science, 220(4598):671–680, 1983

work page 1983
[20]

Boris K ¨opf and David A. Basin. An information-theoretic model for adaptive side-channel attacks. In Peng Ning, Sabrina De Capitani di Vimercati, and Paul F. Syverson, editors, Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007 , pages 286–296. ACM, 2007

work page 2007
[21]

Widespread timing vulnerabilities in o penid implementations

Taylor Nelson. Widespread timing vulnerabilities in o penid implementations. http://lists.openid.net/pipermail/openid-security/2010-July/001156.html , 2010

work page 2010
[22]

Pasareanu, Pasquale Malacaria, and Tevﬁk Bultan

Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevﬁk Bultan. Synthesis of adaptive side-channel attacks. In 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA , 2017

work page 2017
[23]

P˘ as˘ areanu, Quoc-Sang Phan, and Pasquale Malacaria

Corina S. P˘ as˘ areanu, Quoc-Sang Phan, and Pasquale Malacaria. Multi-run side-channel analysis using Symboli c Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium , CSF ’16, Washington, DC, USA, 2016. IEEE Computer Society

work page 2016
[24]

P˘ as˘ areanu, Willem Visser, David Bushnell,Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta

Corina S. P˘ as˘ areanu, Willem Visser, David Bushnell,Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, pages 1–35, 2013

work page 2013
[25]

Rizzo and T

J. Rizzo and T. Duong. The crime attack. Ekoparty Security Conference, 2012

work page 2012
[26]

On the foundations of quantitative information ﬂow

Geoﬀrey Smith. On the foundations of quantitative information ﬂow. In Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS) , 2009

work page 2009

[1] [1]

8299” 63 15 5.906 “1392

INTRODUCTION Modern software systems store and manipulate sensitive inf orma- tion. It is crucial for software developers to write code in a man- ner that prevents disclosure of sensitive information to ar bitrary users. However, computation that accesses sensitive infor mation can have attacker-measurable characteristics that leaks i nforma- tion. This c...

work page 1950

[2] [2]

We consider functions F that take as input a secret string h∈ H and an attacker-controlled string l∈ L and that have side-channel observations o∈ O

AUTOMATIC ATTACK SYNTHESIS In this section we give a two phase approach that synthesizes attacks (Procedure 1). We consider functions F that take as input a secret string h∈ H and an attacker-controlled string l∈ L and that have side-channel observations o∈ O. Procedure 1 SynthesizeAttack(F (h, l), Ch, h∗ ) This procedure calls the GenerateConstraints and...

work page

[3] [3]

In the following discussion, H, L, and O are random variables repre- senting high-security input, low-security input, and side -channel observation respectively

ENTROPY-BASED OBJECTIVE FUNCTION Here we derive an objective function to measure the amount of in- formation an attacker expects to gain by choosing an input va lue lval to be used in the attack search heuristics of Section 4. In the following discussion, H, L, and O are random variables repre- senting high-security input, low-security input, and side -ch...

work page

[4] [4]

temperature

ATTACK SYNTHESIS HEURISTICS At every attack step the goal is to choose a low input l∗ that re- veals information about h∗ . Here we describe diﬀerent techniques for synthesizing attack inputs l∗ . Each approach uses a diﬀerent heuristic to explore a subset of the possible low inputs. To s earch the input space eﬃciently, we ﬁrst observe that we need to re...

work page

[5] [5]

We implemented Procedure 2 using Symbolic Path Finder (SPF) [16]

IMPLEMENTATIONS AND EXPERIMENTS Implementation. We implemented Procedure 2 using Symbolic Path Finder (SPF) [16]. We implemented Procedure 3 as a Java program that takes the observation constraints generated b y Pro- cedure 2 as input, along with Ch and h∗ . The variations of At- tackInput from Section 4 (Procedures 4, 5, and 6) are imple- mented in Java....

work page

[6] [6]

We present the mean values of the results in Tables 4

We ran each experiment for 5 randomly chosen secrets. We present the mean values of the results in Tables 4. For RA, we s et the sample size K to 20. For SA, we set the temperature range ( t to tmin) from 10 to 0.001 and cooling rate k as 0.1. For GA, we set population size popSize to 20, oﬀspring size as 10, number of best selections N as 10. Results. In...

work page

[7] [7]

There has been recent results on synthesizing attacks or qua nti- fying information leakage under a model where the attacker c an make multiple runs of the system [2, 3, 6, 12, 15]

RELATED WORK There has been prior work on analyzing side-channels [2, 4, 5 , 15]. There has been recent results on synthesizing attacks or qua nti- fying information leakage under a model where the attacker c an make multiple runs of the system [2, 3, 6, 12, 15]. For example , LeakWatch [6] estimates leakage in Java programs based on sa m- pling program e...

work page

[8] [8]

CONCLUSION In this paper we presented techniques for synthesizing adap tive attacks for string manipulating programs. To the best of our knowledge this is the ﬁrst work which is able to automaticall y dis- cover side channel vulnerabilities by synthesizing attacks targeting string manipulating functions. We presented several heuri stics for attack synthes...

work page

[9] [9]

Automata-based model counting for string constraints

Abdulbaki Aydin, Lucas Bang, and Tevﬁk Bultan. Automata-based model counting for string constraints. In Proceedings of the 27th International Conference on Computer Aided Veriﬁcation (CA V), pages 255–272, 2015

work page 2015

[10] [10]

Pasareanu, and Tevﬁk Bultan

Lucas Bang, Abdulbaki Aydin, Quoc-Sang Phan, Corina S. Pasareanu, and Tevﬁk Bultan. String analysis for side channels with segmented oracles. In Proceedings of the 24th ACM SIGSOFT International Symposium on the Foundations of Software Engineering , 2016

work page 2016

[11] [11]

Online synthesis of adaptive side-channel attacks based on noisy observations

Lucas Bang, Nicolas Rosner, and Tevﬁk Bultan. Online synthesis of adaptive side-channel attacks based on noisy observations. In Proceedings of the IEEE European Symposium on Security and Privacy (EuroS&P) , 2018

work page 2018

[12] [12]

Remote Timing Attacks Are Practical

David Brumley and Dan Boneh. Remote Timing Attacks Are Practical. In Proceedings of the 12th Conference on USENIX Security Symposium - Volume 12 , SSYM’03, pages 1–1, Berkeley, CA, USA, 2003. USENIX Association

work page 2003

[13] [13]

Side-channel leaks in web applications: A reality today, a challenge tomorrow

Shuo Chen, Rui Wang, XiaoFeng Wang, and Kehuan Zhang. Side-channel leaks in web applications: A reality today, a challenge tomorrow. In Proceedings of the 2010 IEEE Symposium on Security and Privacy , SP ’10, pages 191–206, Washington, DC, USA, 2010. IEEE Computer Society

work page 2010

[14] [14]

Leakwatch: Estimating information leakage from java programs

Tom Chothia, Yusuke Kawamoto, and Chris Novakovic. Leakwatch: Estimating information leakage from java programs. In Computer Security - ESORICS 2014 - 19th European Symposium on Research in Computer Security, Wroclaw, Poland, September 7-11, 2014. Proceedings, Part II, pages 219–236, 2014

work page 2014

[15] [15]

Cover and Joy A

Thomas M. Cover and Joy A. Thomas. Elements of Information Theory (Wiley Series in Telecommunications and Signal Processing) . Wiley-Interscience, 2006

work page 2006

[16] [16]

Time trial: Racing towards practical remote timing attacks

Joel Sandin Daniel Mayer. Time trial: Racing towards practical remote timing attacks. https://www.nccgroup.trust/globalassets/our-research/us/whitepapers/TimeTrial.pdf, 2014

work page 2014

[17] [17]

Genetic algorithms in search, optimization, and machine learning

David E Goldberg. Genetic algorithms in search, optimization, and machine learning. Technical report, 198 9

work page

[18] [18]

James C. King. Symbolic execution and program testing. Commun. ACM , 19(7):385–394, July 1976

work page 1976

[19] [19]

Optimization by simulated annealing

Scott Kirkpatrick, C Daniel Gelatt, and Mario P Vecchi. Optimization by simulated annealing. science, 220(4598):671–680, 1983

work page 1983

[20] [20]

Boris K ¨opf and David A. Basin. An information-theoretic model for adaptive side-channel attacks. In Peng Ning, Sabrina De Capitani di Vimercati, and Paul F. Syverson, editors, Proceedings of the 2007 ACM Conference on Computer and Communications Security, CCS 2007 , pages 286–296. ACM, 2007

work page 2007

[21] [21]

Widespread timing vulnerabilities in o penid implementations

Taylor Nelson. Widespread timing vulnerabilities in o penid implementations. http://lists.openid.net/pipermail/openid-security/2010-July/001156.html , 2010

work page 2010

[22] [22]

Pasareanu, Pasquale Malacaria, and Tevﬁk Bultan

Quoc-Sang Phan, Lucas Bang, Corina S. Pasareanu, Pasquale Malacaria, and Tevﬁk Bultan. Synthesis of adaptive side-channel attacks. In 30th IEEE Computer Security Foundations Symposium, CSF 2017, Santa Barbara, CA, USA , 2017

work page 2017

[23] [23]

P˘ as˘ areanu, Quoc-Sang Phan, and Pasquale Malacaria

Corina S. P˘ as˘ areanu, Quoc-Sang Phan, and Pasquale Malacaria. Multi-run side-channel analysis using Symboli c Execution and Max-SMT. In Proceedings of the 2016 IEEE 29th Computer Security Foundations Symposium , CSF ’16, Washington, DC, USA, 2016. IEEE Computer Society

work page 2016

[24] [24]

P˘ as˘ areanu, Willem Visser, David Bushnell,Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta

Corina S. P˘ as˘ areanu, Willem Visser, David Bushnell,Jaco Geldenhuys, Peter Mehlitz, and Neha Rungta. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering, pages 1–35, 2013

work page 2013

[25] [25]

Rizzo and T

J. Rizzo and T. Duong. The crime attack. Ekoparty Security Conference, 2012

work page 2012

[26] [26]

On the foundations of quantitative information ﬂow

Geoﬀrey Smith. On the foundations of quantitative information ﬂow. In Proceedings of the 12th International Conference on Foundations of Software Science and Computational Structures (FOSSACS) , 2009

work page 2009