Abstract extensionality: on the properties of incomplete abstract interpretations
| Autor: | Roberta Gori, Roberto Bruni, Isabel Garcia-Contreras, Dusko Pavlovic, Roberto Giacobazzi |
|---|---|
| Jazyk: | angličtina |
| Rok vydání: | 2020 |
| Předmět: |
Computability
Computer science Program analysis Abstract interpretation 020207 software engineering 0102 computer and information sciences 02 engineering and technology 01 natural sciences Algebra Obfuscation (software) symbols.namesake Turing completeness 010201 computation theory & mathematics If and only if Extensionality 0202 electrical engineering electronic engineering information engineering symbols Equivalence (formal languages) Special case Safety Risk Reliability and Quality Software |
| Popis: | In this paper we generalise the notion of extensional (functional) equivalence of programs to abstract equivalences induced by abstract interpretations . The standard notion of extensional equivalence is recovered as the special case, induced by the concrete interpretation. Some properties of the extensional equivalence, such as the one spelled out in Rice’s theorem, lift to the abstract equivalences in suitably generalised forms. On the other hand, the generalised framework gives rise to interesting and important new properties, and allows refined, non-extensional analyses. In particular, since programs turn out to be extensionally equivalent if and only if they are equivalent just for the concrete interpretation, it follows that any non-trivial abstract interpretation uncovers some intensional aspect of programs. This striking result is also effective, in the sense that it allows constructing, for any non-trivial abstraction, a pair of programs that are extensionally equivalent, but have different abstract semantics. The construction is based on the fact that abstract interpretations are always sound, but that they can be made incomplete through suitable code transformations. To construct these transformations, we introduce a novel technique for building incompleteness cliques of extensionally equivalent yet abstractly distinguishable programs: They are built together with abstract interpretations that produce false alarms. While programs are forced into incompleteness cliques using both control-flow and data-flow transformations, the main result follows from limitations of data-flow transformations with respect to control-flow ones. A further consequence is that the class of incomplete programs for a non-trivial abstraction is Turing complete. The obtained results also shed a new light on the relation between the techniques of code obfuscation and the precision in program analysis. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|