Verification of Functional Correctness of Code Diversification Techniques

Autor:	Freek Verbeek, Binoy Ravindran, Jae-Won Jang
Rok vydání:	2021
Předmět:	Correctness Theoretical computer science Computer science InformationSystems_INFORMATIONSTORAGEANDRETRIEVAL Functional equivalence Code (cryptography) Binary number Context (language use) Diversification (marketing strategy) Equivalence (measure theory)
Zdroj:	Lecture Notes in Computer Science ISBN: 9783030763831 NFM
DOI:	10.1007/978-3-030-76384-8_11
Popis:	Code diversification techniques are popular code-reuse attacks defense. The majority of code diversification research focuses on analyzing non-functional properties, such as whether the technique improves security. This paper provides a methodology to verify functional equivalence between the original and a diversified binary. We present a formal notion of binary equivalence resilient to diversification. Moreover, an algorithm is presented that checks whether two binaries – one original and one diversified – satisfy that notion of equivalence. The purpose of our work is to allow untrusted diversification techniques in a safety-critical context. We apply the methodology to three state-of-the-art diversification techniques used on the GNU Coreutils package. Overall, results show that our method can prove functional equivalence for 85,315 functions in the analyzed binaries.
Databáze:	OpenAIRE
Externí odkaz:	https://explore.openaire.eu/search/publication?articleId=doi_________::c2f229b4bf7cc2f43e7a56a86811618d https://doi.org/10.1007/978-3-030-76384-8_11 Zobrazit plný text záznamu