×

Specifying imperative data obfuscations. (English) Zbl 1138.68406

Garay, Juan A. (ed.) et al., Information security. 10th international conference, ISC 2007, Valparaíso, Chile, October 9–12, 2007. Proceedings. Berlin: Springer (ISBN 978-3-540-75495-4/pbk). Lecture Notes in Computer Science 4779, 299-314 (2007).
Summary: An obfuscation aims to transform a program, without affecting the functionality, so that some secret information within the program can be hidden for as long as possible from an adversary. Proving that an obfuscating transform is correct (i.e. it preserves functionality) is considered to be a challenging task.
In this paper we show how data refinement can be used to specify imperative data obfuscations. An advantage of this approach is that we can establish a framework in which we can prove the correctness of our obfuscations. We demonstrate our framework by considering some examples from obfuscation literature. We show how to specify these obfuscations, prove that they are correct and produce generalisations.
For the entire collection see [Zbl 1137.68007].

MSC:

68P25 Data encryption (aspects in computer science)
68N99 Theory of software
PDFBibTeX XMLCite
Full Text: DOI