Imperial College London

ProfessorMichaelHuth

Faculty of EngineeringDepartment of Computing

Head of the Department of Computing
 
 
 
//

Contact

 

m.huth Website

 
 
//

Location

 

Huxley 566Huxley BuildingSouth Kensington Campus

//

Summary

 

Publications

Citation

BibTex format

@techreport{Huth:2014:10.25561/95039,
author = {Huth, M and Kuo, JH-P},
booktitle = {Departmental Technical Report: 14/10},
doi = {10.25561/95039},
publisher = {Department of Computing, Imperial College London},
title = {Quantitative threat analysis via a logical service},
url = {http://dx.doi.org/10.25561/95039},
year = {2014}
}

RIS format (EndNote, RefMan)

TY  - RPRT
AB - It is increasingly important to analyze system security quantitatively using concepts suchas trust, reputation, cost, and risk. This requires a thorough understanding of how suchconcepts should interact so that we can validate the assessment of threats, the choice ofadopted risk management, etc.. To this end, we propose a declarative language Peal+ inwhich the interaction of such concepts can be rigorously described and analyzed. Peal+ hasbeen implemented in PEALT using the SMT solver Z3 as analysis back-end. PEALT's codegenerators target complex back-ends and evolve with optimizations or new back-ends. Thuswe can neither trust the tool chain nor feasibly prove correctness of all involved artefacts.We eliminate the need to trust that tool chain by independently certifying scenarios foundby back-ends in a manner agnostic of code generation and choice of back-end. This scenariovalidation is compositional, courtesy of Kleene's 3-valued logic and potential re nement ofscenarios. We prove the correctness of this validation, discuss how PEALT presents scenariosto further users' understanding, and demonstrate the utility of this approach by showing howit can express attack-countermeasure trees so that the interaction of attack success probability,attack cost, and attack impact can be analyzed.
AU - Huth,M
AU - Kuo,JH-P
DO - 10.25561/95039
PB - Department of Computing, Imperial College London
PY - 2014///
TI - Quantitative threat analysis via a logical service
T1 - Departmental Technical Report: 14/10
UR - http://dx.doi.org/10.25561/95039
UR - http://hdl.handle.net/10044/1/95039
ER -