QUAIL: A Quantitative Security Analyzer for Imperative Code

Fabrizio Biondi; Andrzej Wasowski; Louis-Marie Traonouez; Axel Legay

doi:dx.doi.org/10.1007/978-3-642-39799-8_49

QUAIL: A Quantitative Security Analyzer for Imperative Code

Fabrizio Biondi, Andrzej Wasowski, Louis-Marie Traonouez, Axel Legay

Aalborg University

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

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

Original language	English
Title of host publication	Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.
Number of pages	6
Publication date	Jul 2013
Pages	702-707
ISBN (Print)	978-3-642-39798-1
DOIs	https://doi.org/dx.doi.org/10.1007/978-3-642-39799-8_49
Publication status	Published - Jul 2013

Series	Lecture Notes in Computer Science
Volume	8044
ISSN	0302-9743

Keywords

Quantitative Security Analysis
Markov Chain Model
Private Information
Randomized Protocols
Security Protocol Effectiveness

Access to Document

dx.doi.org/10.1007/978-3-642-39799-8_49

MT-Lab - Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.-M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Project: Research

Cite this

@inproceedings{b13d21bd6c434daeba3854b1aa13804c,

title = "QUAIL: A Quantitative Security Analyzer for Imperative Code",

abstract = "Quantitative security analysis evaluates and compares how effectively asystem 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{\textquoteright}s behavior as observed by an attacker, and computes the correlation between the system{\textquoteright}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{\textquoteright}s effectiveness.We experiment with a few examples and show that QUAIL{\textquoteright}s security analysis ismore accurate and revealing than results of other tools",

keywords = "Quantitative Security Analysis, Markov Chain Model, Private Information, Randomized Protocols, Security Protocol Effectiveness, Quantitative Security Analysis, Markov Chain Model, Private Information, Randomized Protocols, Security Protocol Effectiveness",

author = "Fabrizio Biondi and Andrzej Wasowski and Louis-Marie Traonouez and Axel Legay",

year = "2013",

month = jul,

doi = "dx.doi.org/10.1007/978-3-642-39799-8_49",

language = "English",

isbn = "978-3-642-39798-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "702--707",

booktitle = "Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.",

}

QUAIL: A Quantitative Security Analyzer for Imperative Code. / Biondi, Fabrizio; Wasowski, Andrzej; Traonouez, Louis-Marie et al.
Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.. 2013. p. 702-707 (Lecture Notes in Computer Science, Vol. 8044).

Research output: Conference Article in Proceeding or Book/Report chapter › Article in proceedings › Research › peer-review

TY - GEN

T1 - QUAIL: A Quantitative Security Analyzer for Imperative Code

AU - Biondi, Fabrizio

AU - Wasowski, Andrzej

AU - Traonouez, Louis-Marie

AU - Legay, Axel

PY - 2013/7

Y1 - 2013/7

N2 - Quantitative security analysis evaluates and compares how effectively asystem 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 ismore accurate and revealing than results of other tools

AB - Quantitative security analysis evaluates and compares how effectively asystem 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 ismore accurate and revealing than results of other tools

KW - Quantitative Security Analysis

KW - Markov Chain Model

KW - Private Information

KW - Randomized Protocols

KW - Security Protocol Effectiveness

KW - Quantitative Security Analysis

KW - Markov Chain Model

KW - Private Information

KW - Randomized Protocols

KW - Security Protocol Effectiveness

U2 - dx.doi.org/10.1007/978-3-642-39799-8_49

DO - dx.doi.org/10.1007/978-3-642-39799-8_49

M3 - Article in proceedings

SN - 978-3-642-39798-1

T3 - Lecture Notes in Computer Science

SP - 702

EP - 707

BT - Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.

ER -

QUAIL: A Quantitative Security Analyzer for Imperative Code

Abstract

Keywords

Access to Document

Fingerprint

Projects

MT-Lab - Modelling of Information Technology

Cite this