Is Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs

TitleIs Your Software on Dope? - Formal Analysis of Surreptitiously "enhanced" Programs
Publication TypeBook Chapter
Year of Publication2017
AuthorsD'Argenio, PR, Barthe, G, Biewer, S, Finkbeiner, B, Hermanns, H
EditorYang, H
Book TitleProgramming Languages and Systems - 26th European Symposium on Programming, {ESOP} 2017, Held as Part of the European Joint Conferences on Theory and Practice of Software, {ETAPS} 2017, Uppsala, Sweden, April 22-29, 2017, Proceedings
Series TitleLecture Notes in Computer Science
Volume10201
Pagination83–110
PublisherSpringer
ISBN Number978-3-662-54433-4
AbstractUsually, it is the software manufacturer who employs verification or testing to ensure that the software embedded in a device meets its main objectives. However, these days we are confronted with the situation that economical or technological reasons might make a manufacturer become interested in the software slightly deviating from its main objective for dubious reasons. Examples include lock-in strategies and the NOx emission scandals in automotive industry. This phenomenon is what we call software doping. It is turning more widespread as software is embedded in ever more devices of daily use. The primary contribution of this article is to provide a hierarchy of simple but solid formal definitions that enable to distinguish whether a program is clean or doped. Moreover, we show that these characterisations provide an immediate framework for analysis by using already existing verification techniques. We exemplify this by applying self-composition on sequential programs and model checking of HyperLTL formulas on reactive models.
URLhttp://dx.doi.org/10.1007/978-3-662-54434-1_4
DOI10.1007/978-3-662-54434-1_4
PDF (Full text):