| Reference : To verify or tolerate, that’s the question |
| Scientific congresses, symposiums and conference proceedings : Unpublished conference | |||
| Engineering, computing & technology : Computer science | |||
| Security, Reliability and Trust | |||
| http://hdl.handle.net/10993/50425 | |||
| To verify or tolerate, that’s the question | |
| English | |
Pinto Gouveia, Ines  [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >] | |
| Sakr, Mouhammad [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >] | |
| Graczyk, Rafal [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >] | |
| Volp, Marcus [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >] | |
| 6-Dec-2021 | |
| Yes | |
| International | |
| Program Analysis and Verification on Trusted Platforms (PAVeTrust) Workshop (co-located with ACSAC21) | |
| 6-12-2021 | |
| [en] TEE ; verifcation ; resilience | |
| [en] Formal verification carries the promise of absolute correctness,
guaranteed at the highest level of assurance known today. However, inherent to many verification attempts is the assumption that the underlying hardware, the code-generation toolchain and the verification tools are correct, all of the time. While this assumption creates interesting recursive verification challenges, which already have been executed successfully for all three of these elements, the coverage of this assumption remains incomplete, in particular for hardware. Accidental faults, such as single-event upsets, transistor aging and latchups keep causing hardware to behave arbitrarily in situations where such events occur and require other means (e.g., tolerance) to safely operate through them. Targeted attacks, especially physical ones, have a similar potential to cause havoc. Moreover, faults of the above kind may well manifest in such a way that their effects extend to all software layers, causing incorrect behavior, even in proven correct ones. In this position paper, we take a holistic system-architectural point of view on the role of trusted-execution environments (TEEs), their implementation complexity and the guarantees they can convey and that we want to be preserved in the presence of faults. We find that if absolute correctness should remain our visionary goal, TEEs can and should be constructed differently with tolerance embedded at the lowest levels and with verification playing an essential role. Verification should both assure the correctness of the TEE construction protocols and mechanisms as well as help protecting the applications executing inside the TEEs. | |
| Interdisciplinary Centre for Security, Reliability and Trust (SnT) > Critical and Extreme Security and Dependability Research Group (CritiX) | |
| http://hdl.handle.net/10993/50425 | |
| FnR ; FNR12686210 > Marcus Völp > HyLIT > Architectural Support For Intrusion Tolerant Operating-system Kernels > 01/11/2018 > 31/10/2021 > 2018 |
| File(s) associated to this reference | ||||||||||||||
|
Fulltext file(s):
| ||||||||||||||
All documents in ORBilu are protected by a user license.
