Systematic design of program transformation frameworks by abstract interpretation

AbstractTo alleviate the inefficiencies caused by the interaction of the logic and functional sides, integrated languages may take advantage of demand information, i.e. knowing in advance which computations are needed and, to which extent, in a particular context. This work studies demand analysis – which is closely related to backwards strictness analysis – in a semantic framework of partial predicates, which in turn are constructive realizations of ideals in a domain. This will allow us to give a concise, unified presentation of demand analysis, to relate it to other analyses based on abstract interpretation or strictness logics, some hints for the implementation, and, more important, to prove the soundness of our analysis based on demand equations. There are also some innovative results. One of them is that a set constraint-based analysis has been derived in a stepwise manner using ideas taken from the area of program transformation. The other one is the possibility of using program transformation itself to perform the analysis, specially in those domains of properties where algorithms based on constraint solving are too weak.

Download Full-text

Theoretical Aspects of Semantics-Based Language Implementation

DAIMI Report Series ◽

10.7146/dpb.v19i329.6561 ◽

1990 ◽

Vol 19 (329) ◽

Author(s):

Flemming Nielson

Keyword(s):

Programming Languages ◽

Program Analysis ◽

Code Generation ◽

Program Transformation ◽

Abstract Interpretation ◽

Language Implementation

The research summarised here concerns theoretical aspects involved in the implementation of programming languages directly from a description of their semantics. This involves a study of the subtasks abstract interpretation (a framework for program analysis), code generation and program transformation and the main aim has been to ensure the correctness of these subtasks.

Download Full-text

Semantics-based software watermarking by abstract interpretation

Mathematical Structures in Computer Science ◽

10.1017/s0960129518000038 ◽

2018 ◽

Vol 29 (2) ◽

pp. 339-388

Author(s):

MILA DALLA PREDA ◽

MICHELE PASQUA

Keyword(s):

Program Analysis ◽

Program Transformation ◽

Abstract Interpretation ◽

Semantic Property ◽

Software Protection ◽

Formal Framework ◽

Software Watermarking ◽

Watermarking Scheme ◽

Quality Features

Software watermarking is a software protection technique used to defend the intellectual property of proprietary code. In particular, software watermarking aims at preventing software piracy by embedding a signature, i.e. an identifier reliably representing the owner, in the code. When an illegal copy is made, the owner can claim his/her identity by extracting the signature. It is important to hide the signature in the program in order to make it difficult for the attacker to detect, tamper or remove it. In this work, we present a formal framework for software watermarking, based on program semantics and abstract interpretation, where attackers are modelled as abstract interpreters. In this setting, we can prove that the ability to identify signatures can be modelled as a completeness property of the attackers in the abstract interpretation framework. Indeed, hiding a signature in the code corresponds to embed it as a semantic property that can be retrieved only by attackers that are complete for it. Any abstract interpreter that is not complete for the property specifying the signature cannot detect, tamper or remove it. We formalize in the proposed framework the major quality features of a software watermarking technique: secrecy, resilience, transparence and accuracy. This provides a unifying framework for interpreting both watermarking schemes and attacks, and it allows us to formally compare the quality of different watermarking techniques. Indeed, a large number of watermarking techniques exist in the literature and they are typically evaluated with respect to their secrecy, resilience, transparence and accuracy to attacks. Formally identifying the attacks for which a watermarking scheme is secret, resilient, transparent or accurate can be a complex and error-prone task, since attacks and watermarking schemes are typically defined in different settings and using different languages (e.g. program transformation vs. program analysis), complicating the task of comparing one against the others.

Download Full-text

The Systematic Design of Responsibility Analysis by Abstract Interpretation

ACM Transactions on Programming Languages and Systems ◽

10.1145/3484938 ◽

2022 ◽

Vol 44 (1) ◽

pp. 1-90

Author(s):

Chaoqiang Deng ◽

Patrick Cousot

Keyword(s):

Program Analysis ◽

Abstract Interpretation ◽

Systematic Design ◽

Causality Analysis ◽

Critical Importance ◽

Single Action ◽

Root Cause ◽

Innovative Idea ◽

Trace Semantics ◽

Definition Of

Given a behavior of interest, automatically determining the corresponding responsible entity (i.e., the root cause) is a task of critical importance in program static analysis. In this article, a novel definition of responsibility based on the abstraction of trace semantics is proposed, which takes into account the cognizance of observer, which, to the best of our knowledge, is a new innovative idea in program analysis. Compared to current dependency and causality analysis methods, the responsibility analysis is demonstrated to be more precise on various examples. However, the concrete trace semantics used in defining responsibility is uncomputable in general, which makes the corresponding concrete responsibility analysis undecidable. To solve this problem, the article proposes a sound framework of abstract responsibility analysis, which allows a balance between cost and precision. Essentially, the abstract analysis builds a trace partitioning automaton by an iteration of over-approximating forward reachability analysis with trace partitioning and under/over-approximating backward impossible failure accessibility analysis, and determines the bounds of potentially responsible entities along paths in the automaton. Unlike the concrete responsibility analysis that identifies exactly a single action as the responsible entity along every concrete trace, the abstract analysis may lose some precision and find multiple actions potentially responsible along each automaton path. However, the soundness is preserved, and every responsible entity in the concrete is guaranteed to be also found responsible in the abstract.

Download Full-text