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 mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >]
Sakr, Mouhammad mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >]
Graczyk, Rafal mailto [University of Luxembourg > Interdisciplinary Centre for Security, Reliability and Trust (SNT) > CritiX >]
Volp, Marcus mailto [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):

FileCommentaryVersionSizeAccess
Open access
verify_or_tolerate.pdfPublisher postprint643.87 kBView/Open

Bookmark and Share SFX Query

All documents in ORBilu are protected by a user license.