Small faults grow up - Verification of error masking robustness in arithmetically encoded programs

Publikation: Beitrag in Buch/Bericht/KonferenzbandBeitrag in einem Konferenzband

Abstract

The increasing prevalence of soft errors and security concerns due to recent attacks like rowhammer have caused increased interest in the robustness of software against bit flips. Arithmetic codes can be used as a protection mechanism to detect small errors injected in the program’s data. However, the accumulation of propagated errors can increase the number of bits flips in a variable - possibly up to an undetectable level. The effect of error masking can occur: An error weight exceeds the limitations of the code and a new, valid, but incorrect code word is formed. Masked errors are undetectable, and it is crucial to check variables for bit flips before error masking can occur. In this paper, we develop a theory of provably robust arithmetic programs. We focus on the interaction of bit flips that can happen at different locations in the program and the propagation and possible masking of errors. We show how this interaction can be formally modeled and how off-the-shelf model checkers can be used to show correctness. We evaluate our approach based on prominent and security relevant algorithms and show that even multiple faults injected at any time into any variables can be handled by our method.

Originalspracheenglisch
TitelVerification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
Redakteure/-innenRuzica Piskac, Constantin Enea
Herausgeber (Verlag)Springer
Seiten183-204
Seitenumfang22
ISBN (elektronisch)978-3-030-11245-5
ISBN (Print)978-3-030-11244-8
DOIs
PublikationsstatusVeröffentlicht - 2019
Veranstaltung2019 International Conference on Verification, Model Checking, and Abstract Interpretation - Cascais, Portugal
Dauer: 13 Jan 201915 Jan 2019

Publikationsreihe

NameLecture Notes in Computer Science
Band11388

Konferenz

Konferenz2019 International Conference on Verification, Model Checking, and Abstract Interpretation
KurztitelVMCAI 2019
LandPortugal
OrtCascais
Zeitraum13/01/1915/01/19

ASJC Scopus subject areas

  • !!Theoretical Computer Science
  • !!Computer Science(all)

Fingerprint Untersuchen Sie die Forschungsthemen von „Small faults grow up - Verification of error masking robustness in arithmetically encoded programs“. Zusammen bilden sie einen einzigartigen Fingerprint.

Dieses zitieren