CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Fault-resilient non-interference

Filippo Del Tedesco ; David Sands (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)) ; Alejandro Russo (Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers))
29th IEEE Computer Security Foundations Symposium, CSF 2016, Lisbon, Portugal, 27 June - 1 July 2016 (1940-1434). p. 401-416. (2016)
[Konferensbidrag, refereegranskat]

Environmental noise (e.g. heat, ionized particles, etc.) causes transient faults in hardware, which lead to corruption of stored values. Mission-critical devices require such faults to be mitigated by fault-tolerance - a combination of techniques that aim at preserving the functional behaviour of a system despite the disruptive effects of transient faults. Fault-tolerance typically has a high deployment cost - special hardware might be required to implement it - and provides weak statistical guarantees. It is also based on the assumption that faults are rare. In this paper, we consider scenarios where security, rather than functional correctness, is the main asset to be protected. Our main contribution is a theory for expressing confidentiality of data in the presence of transient faults. We show that the natural probabilistic definition of security in the presence of faults can be captured by a possibilistic definition. Furthermore, the possibilistic definition is implied by a known bisimulation-based property, called Strong Security. We illustrate the utility of these results for a simple RISC architecture for which only the code memory and program counter are assumed fault-tolerant. We present a type-directed compilation scheme that produces RISC code from a higher-level language for which Strong Security holds - i.e. well-typed programs compile to RISC code which is secure despite transient faults. In contrast with fault-tolerance solutions, our technique assumes relatively little special hardware, gives formal guarantees, and works in the presence of an active attacker who aggressively targets parts of a system and induces faults precisely.

Nyckelord: faults, Non-interference



Denna post skapades 2016-12-19. Senast ändrad 2017-09-14.
CPL Pubid: 246292

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, Programvaruteknik (Chalmers)

Ämnesområden

Datavetenskap (datalogi)

Chalmers infrastruktur