Code obfuscation is a software security technique where transformations are applied
to source and/or machine code to make them more difficult to analyze and understand
to deter reverse-engineering and tampering. However, in many commercial tools, such
as Irdeto's Cloakware product, it is not clear why the end user should believe that
the programs that come out the other end are still the same program"!
In this thesis, we apply techniques of formal specification and verification, by
using the Coq Proof Assistant and IMP (a simple imperative language within it), to
formulate what it means for a program's semantics to be preserved by an obfuscating
transformation, and give formal machine-checked proofs that these properties hold.
We describe our work on opaque predicate and control flow flattening transformations.
Along the way, we also employ Hoare logic as an alternative to state equivalence,
as well as augment the IMP program with Switch statements. We also define a lower-level flowchart language to wrap around IMP for modelling certain flattening
transformations, treating blocks of codes as objects in their own right.
We then discuss related work in the literature on formal verification of data obfuscation
and layout obfuscation transformations in IMP, and conclude by discussing
CompCert, a formally verified C compiler in Coq, along with work that has been done
on obfuscation there, and muse on the possibility of implementing formal methods in
the next generation of real-world obfuscation tools.
| Identifer | oai:union.ndltd.org:uottawa.ca/oai:ruor.uottawa.ca:10393/39994 |
| Date | 20 December 2019 |
| Creators | Lu, Weiyun |
| Contributors | Felty, Amy, Scott, Philip |
| Publisher | Université d'Ottawa / University of Ottawa |
| Source Sets | Université d’Ottawa |
| Language | English |
| Detected Language | English |
| Type | Thesis |
| Format | application/pdf |
Page generated in 0.0021 seconds