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 Universitet

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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

Originalsprog	Engelsk
Titel	Computer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.
Antal sider	6
Publikationsdato	jul. 2013
Sider	702-707
ISBN (Trykt)	978-3-642-39798-1
DOI	https://doi.org/dx.doi.org/10.1007/978-3-642-39799-8_49
Status	Udgivet - jul. 2013

Navn	Lecture Notes in Computer Science
Vol/bind	8044
ISSN	0302-9743

Emneord

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

Adgang til dokumentet

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
Projekter: Projekt › Forskning

Citationsformater

@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. s. 702-707 (Lecture Notes in Computer Science, Bind 8044).

Publikation: Konference artikel i Proceeding eller bog/rapport kapitel › Konferencebidrag i proceedings › Forskning › 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

Emneord

Adgang til dokumentet

Fingeraftryk

Projekter

MT-Lab - Modelling of Information Technology

Citationsformater