Blogs (1) >>
POPL 2019
Sun 13 - Sat 19 January 2019 Cascais, Portugal
Mon 14 Jan 2019 14:30 - 15:00 at Sala XII - Research Papers: Program Verification Chair(s): Chris Hawblitzel

The insertion of expressions mixing arithmetic operators and bitwise boolean operators is a widespread protection of sensitive data in source programs. This recent advanced obfuscation technique is one of the less studied among program obfuscations even if it is commonly found in binary code. In this paper, we formally verify in Coq this data obfuscation. It operates over a generic notion of mixed boolean-arithmetic expressions and on properties of bitwise operators operating over machine integers. Our obfuscation performs two kinds of program transformations: rewriting of expressions and insertion of modular inverses. To facilitate its proof of correctness, we define boolean semantic tables, a data structure inspired from truth tables. Our obfuscation is integrated into the CompCert formally verified compiler where it operates over Clight programs. The automatic extraction of our program obfuscator into OCaml yields a program with competitive results.

Mon 14 Jan

Displayed time zone: Belfast change

14:00 - 15:30
Research Papers: Program VerificationCPP at Sala XII
Chair(s): Chris Hawblitzel Microsoft Research
14:00
30m
Research paper
Formally Verified Big Step Semantics out of x86-64 Binaries
CPP
Ian Roessle Virginia Tech, USA, Freek Verbeek Open University of the Netherlands, The Netherlands, Binoy Ravindran Virginia Tech
DOI
14:30
30m
Research paper
Formal Verification of a Program Obfuscation Based on Mixed Boolean-Arithmetic Expressions
CPP
Sandrine Blazy Univ Rennes- IRISA, Rémi Hutin IRISA / ENS Rennes
DOI
15:00
30m
Research paper
From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server
CPP
Nicolas Koh , Yao Li University of Pennsylvania, Yishuai Li University of Pennsylvania, Li-yao Xia University of Pennsylvania, Lennart Beringer Princeton University, Wolf Honore , William Mansky University of Illinois at Chicago, Benjamin C. Pierce University of Pennsylvania, Steve Zdancewic University of Pennsylvania
DOI