QUAIL: A Quantitative Security Analyzer for Imperative Code
- Fabrizio Biondi,
- ,
- Louis-Marie Traonouez,
- Axel Legay
- ,
- Aalborg University
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-review
Open access
Publication Information
Output type
Research Output:
Conference Article in Proceeding or Book/Report chapter
Article in proceedings
Peer-reviewOriginal language
EnglishPages from-to (Number of pages)
Pages 702-707 (6 pages)Publication milestones
- Published - 07/2013
Publication status
Published - 07/2013
Book series
- Book series name: Lecture Notes in Computer Science
Volume: 8044
ISSN: 0302-9743
ISBN (Print)
978-3-642-39798-1Publication IDs
- Scopus: 84881179911
Host publication title
Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.Abstract
Quantitative security analysis evaluates and compares how effectively a
system protects its secret data. We introduce QUAIL, the first tool able to perform an arbitrary-precision quantitative analysis of the security of a system depending on private information. QUAIL builds a Markov Chain model of the system’s behavior as observed by an attacker, and computes the correlation between the system’s observable output and the behavior depending on the private information, obtaining the expected amount of bits of the secret that the attacker will infer by observing the system. QUAIL is able to evaluate the safety of randomized protocols depending on secret data, allowing to verify a security protocol’s effectiveness.
We experiment with a few examples and show that QUAIL’s security analysis is
more accurate and revealing than results of other tools
system protects its secret data. We introduce QUAIL, the first tool able to perform an arbitrary-precision quantitative analysis of the security of a system depending on private information. QUAIL builds a Markov Chain model of the system’s behavior as observed by an attacker, and computes the correlation between the system’s observable output and the behavior depending on the private information, obtaining the expected amount of bits of the secret that the attacker will infer by observing the system. QUAIL is able to evaluate the safety of randomized protocols depending on secret data, allowing to verify a security protocol’s effectiveness.
We experiment with a few examples and show that QUAIL’s security analysis is
more accurate and revealing than results of other tools
Publication metrics
PlumX, opens in new tab
Captures
10
Citations
29