Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Tue 15 Jan 2019 15:00 - 15:30 at Sala III - Software Verification Chair(s): Grigory Fedyukovich

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

Tue 15 Jan

VMCAI-2019
14:00 - 15:30: VMCAI 2019 - Software Verification at Sala III
Chair(s): Grigory FedyukovichPrinceton University
VMCAI-201914:00 - 14:30
Talk
Tianhan LuUniversity of Colorado Boulder, Pavol CernyUniversity of Colorado Boulder, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Ashutosh Trivedi
VMCAI-201914:30 - 15:00
Talk
Quentin Bouillaguet, François BobotCEA, Mihaela SighireanuIRIF, University Paris Diderot and CNRS, France, Boris YakobowskiCEA - LIST
File Attached
VMCAI-201915:00 - 15:30
Talk
Anja KarlInstitute of Applied Information Processing and Communications, Graz University of Technology, Robert Schilling, Roderick BloemInstitute of Software Technology, Graz University of Technology , Stefan Mangard