你的软件有问题吗？秘密“增强”程序的形式化分析
Is your software on dope? Formal analysis of surreptitiously "enhanced" programs
摘要：
通常，软件制造商采用验证或测试来确保嵌入在设备中的软件满足其主要目标。然而，这些天来，我们面临的情况是，经济或技术的原因可能会使制造商成为有兴趣的软件稍微偏离其主要目标的可疑原因。例子包括锁定战略和汽车行业的$\mathrm{NO}_x$排放丑闻。这种现象我们称之为软件兴奋剂。随着越来越多的软件被嵌入到日常使用的设备中，它变得越来越普遍。本文的主要贡献是提供了一个简单但可靠的形式化定义的层次结构，可以区分程序是干净的还是掺杂的。此外，我们表明，这些特征提供了一个直接的框架，通过使用现有的验证技术进行分析。我们通过在顺序程序上应用自组合和在反应模型上应用HyperLTL公式的模型检验来验证这一点。
英文摘要：
Usually, 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 $\mathrm{NO}_x$ 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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
