Name
Abstract | ||
|---|---|---|
Many high-level functional programming languages are compiled to or interoperate with, low-level languages such as C and assembly. Research into the security of these compilation and interoperation mechanisms often makes use of high-level attacker models to simplify formalisations. In practice, however, the validity of such high-level attacker models is frequently called into question. In this paper we formally prove that a light-weight ML equipped with a reflection operator can serve as an accurate model for malicious assembly language programs, when reasoning about the security threats such an attacker model poses to the abstractions of ML programs that reside within a protected memory space. The proof proceeds by relating bisimulations over the assembly language attacker and the high-level attacker. |
Year | DOI | Venue |
|---|---|---|
2015 | 10.1007/978-3-319-25942-0_11 | SETTA |
Field | DocType | Volume |
Attack model,Programming language,Abstraction,Functional programming,Computer security,Computer science,Interoperability,Interoperation,Assembly language,Operator (computer programming),Type safety | Conference | 9409 |
ISSN | Citations | PageRank |
0302-9743 | 0 | 0.34 |
References | Authors | |
13 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Adriaan Larmuseau | 1 | 12 | 1.92 |
| Marco Patrignani | 2 | 116 | 11.58 |
| Dave Clarke | 3 | 416 | 26.19 |