Is Your Software on Dope?

DOI10.1007/978-3-662-54434-1_4MaRDI QIDQ2988635zbMATH OpenOpenAlexFDO

Authors Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns, P. R. D'Argenio

Publication date 19 May 2017

Published in Programming Languages and Systems (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1702.04693

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Abstract: 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.

Recommendations

• scientific article; zbMATH DE number 1759991
• Product programs in the wild: retrofitting program verifiers to check information flow security
• scientific article; zbMATH DE number 1808257
• scientific article; zbMATH DE number 4078761
• Information Security and Cryptology - ICISC 2005
• scientific article; zbMATH DE number 1842483

Cites work

• scientific article; zbMATH DE number 3574936 (Why is no real title available?)
• scientific article; zbMATH DE number 6851935 (Why is no real title available?)
• Abstract non-interference
• Algorithms for model checking HyperLTL and HyperCTL^*
• Continuity analysis of programs
• Higher-order approximate relational refinement types for mechanism design and differential privacy
• Relational separation logic
• Secure information flow by self-composition
• Simple relational correctness proofs for static analyses and program transformations
• Static Analysis

Cited in

(5)

• Team semantics for the specification and verification of hyperproperties
• Explaining Hyperproperty Violations
• AutoHyper: explicit-state model checking for HyperLTL
• Deciding hyperproperties combined with functional specifications
• Predicate abstraction for hyperliveness verification

Describes a project that uses

Uses Software

• SymDiff

This page was built for publication: Is Your Software on Dope?

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2988635)