QUAIL: A Quantitative Security Analyzer for Imperative Code

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

Publikation: Konference artikel i Proceeding eller bog/rapport kapitelKonferencebidrag i proceedingsForskningpeer 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
OriginalsprogEngelsk
TitelComputer Aided Verification - 25th International Conference, CAV 2013, Saint Petersburg, Russia, July 13-19, 2013. Proceedings.
Antal sider6
Publikationsdatojul. 2013
Sider702-707
ISBN (Trykt)978-3-642-39798-1
DOI
StatusUdgivet - jul. 2013
NavnLecture Notes in Computer Science
Vol/bind8044
ISSN0302-9743

Fingeraftryk

Dyk ned i forskningsemnerne om 'QUAIL: A Quantitative Security Analyzer for Imperative Code'. Sammen danner de et unikt fingeraftryk.

Citationsformater