Paper Info
Title
Fully abstract trace semantics for low-level isolation mechanisms
Abstract
Many software systems adopt isolation mechanisms of modern processors as software security building blocks. Reasoning about these building blocks means reasoning about elaborate assembly code, which can be very complex due to the loose structure of the code. A way to overcome this complexity is giving the code a more structured semantics. This paper presents one such semantics, namely a fully abstract trace semantics, for an assembly language enhanced with protection mechanisms of modern processors. The trace semantics represents the behaviour of protected assembly code with simple abstractions, unburdened by low-level details, at the maximum degree of precision. Additionally, it captures the capabilities of attackers to protected software and simplifies providing a secure compiler targeting that language.
Year
DOI
Venue
2014
10.1145/2554850.2554865
SAC
Keywords
Field
DocType
software/program verification,computer science,synchronization
Static program analysis,Operational semantics,Programming language,Software security assurance,Computer science,Denotational semantics,Failure semantics,Assembly language,Compiler,Well-founded semantics
Conference
Citations 
PageRank 
References 
8
0.49
16
Authors
2
Name
Order
Citations
PageRank
Marco Patrignani111611.58
Dave Clarke241626.19