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

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

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.

Original languageEnglish
Title of host publicationVerification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings
EditorsRuzica Piskac, Constantin Enea
PublisherSpringer
Pages183-204
Number of pages22
ISBN (Electronic)978-3-030-11245-5
ISBN (Print)978-3-030-11244-8
DOIs
Publication statusPublished - 2019
Event2019 International Conference on Verification, Model Checking, and Abstract Interpretation - Cascais, Portugal
Duration: 13 Jan 201915 Jan 2019

Publication series

NameLecture Notes in Computer Science
Volume11388

Conference

Conference2019 International Conference on Verification, Model Checking, and Abstract Interpretation
Abbreviated titleVMCAI 2019
CountryPortugal
CityCascais
Period13/01/1915/01/19

Fingerprint

Masking
Fault
Robustness
Flip
Soft Error
Interaction
Correctness
Exceed
Attack
Valid
Propagation
Software
Evaluate

Keywords

  • Arithmetic codes
  • Error detection codes
  • Error masking
  • Fault injection
  • Formal verification

ASJC Scopus subject areas

  • Theoretical Computer Science
  • Computer Science(all)

Cite this

Karl, A. F., Schilling, R., Bloem, R., & Mangard, S. (2019). Small faults grow up - Verification of error masking robustness in arithmetically encoded programs. In R. Piskac, & C. Enea (Eds.), Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings (pp. 183-204). (Lecture Notes in Computer Science; Vol. 11388). Springer. https://doi.org/10.1007/978-3-030-11245-5_9

Small faults grow up - Verification of error masking robustness in arithmetically encoded programs. / Karl, Anja Felicitas; Schilling, Robert; Bloem, Roderick; Mangard, Stefan.

Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. ed. / Ruzica Piskac; Constantin Enea. Springer, 2019. p. 183-204 (Lecture Notes in Computer Science; Vol. 11388).

Research output: Chapter in Book/Report/Conference proceedingConference contributionResearchpeer-review

Karl, AF, Schilling, R, Bloem, R & Mangard, S 2019, Small faults grow up - Verification of error masking robustness in arithmetically encoded programs. in R Piskac & C Enea (eds), Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. Lecture Notes in Computer Science, vol. 11388, Springer, pp. 183-204, 2019 International Conference on Verification, Model Checking, and Abstract Interpretation , Cascais, Portugal, 13/01/19. https://doi.org/10.1007/978-3-030-11245-5_9
Karl AF, Schilling R, Bloem R, Mangard S. Small faults grow up - Verification of error masking robustness in arithmetically encoded programs. In Piskac R, Enea C, editors, Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. Springer. 2019. p. 183-204. (Lecture Notes in Computer Science). https://doi.org/10.1007/978-3-030-11245-5_9
Karl, Anja Felicitas ; Schilling, Robert ; Bloem, Roderick ; Mangard, Stefan. / Small faults grow up - Verification of error masking robustness in arithmetically encoded programs. Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings. editor / Ruzica Piskac ; Constantin Enea. Springer, 2019. pp. 183-204 (Lecture Notes in Computer Science).
@inproceedings{12bf9ac1060f48909ee787683dc0aed3,
title = "Small faults grow up - Verification of error masking robustness in arithmetically encoded programs",
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.",
keywords = "Arithmetic codes, Error detection codes, Error masking, Fault injection, Formal verification",
author = "Karl, {Anja Felicitas} and Robert Schilling and Roderick Bloem and Stefan Mangard",
year = "2019",
doi = "10.1007/978-3-030-11245-5_9",
language = "English",
isbn = "978-3-030-11244-8",
series = "Lecture Notes in Computer Science",
publisher = "Springer",
pages = "183--204",
editor = "Ruzica Piskac and Constantin Enea",
booktitle = "Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings",

}

TY - GEN

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

AU - Karl, Anja Felicitas

AU - Schilling, Robert

AU - Bloem, Roderick

AU - Mangard, Stefan

PY - 2019

Y1 - 2019

N2 - 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.

AB - 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.

KW - Arithmetic codes

KW - Error detection codes

KW - Error masking

KW - Fault injection

KW - Formal verification

UR - http://www.scopus.com/inward/record.url?scp=85061102985&partnerID=8YFLogxK

U2 - 10.1007/978-3-030-11245-5_9

DO - 10.1007/978-3-030-11245-5_9

M3 - Conference contribution

SN - 978-3-030-11244-8

T3 - Lecture Notes in Computer Science

SP - 183

EP - 204

BT - Verification, Model Checking, and Abstract Interpretation - 20th International Conference, VMCAI 2019, Proceedings

A2 - Piskac, Ruzica

A2 - Enea, Constantin

PB - Springer

ER -