Abstract The rapid progress of quantum technologies, fostered by the efforts of both academia and industry, has stimulated the design of quantum programming languages and the development of methods to support their verification and optimization. As in the classical setting, static analysis plays a fundamental role in such an endeavour. In this paper, we provide a survey on static analysis approaches for quantum programs, which have been proposed in the literature, distinguishing between dataflow-oriented approaches, which are based on a graph representation of the program information flow, and domain-oriented approaches, which essentially consist of the definition of some appropriate abstract domains representing the program property to be analysed. To illustrate these two perspectives concretely, we also present in detail two specific analyses: a dataflow analysis for managing quantum variables and uncomputation, and a static analysis based on abstract interpretation for detecting state entanglement.

In modern computing systems, preventing sensitive information leakage is a crucial issue. Indeed, to deploy secure computing systems, data protection is an aspect that cannot be ignored. Many security requirements are adopted in this respect, such as opacity and non-interference . The first assures that the truth value of a predicate is masked during computation, while the second prevents confidential information is leaked through uncontrolled system components. Unfortunately, despite their simple intended meaning, confidentiality notions are quite difficult requirements to enforce. In fact, they are actually hyperproperties , and thus require enforcing mechanisms that reason on multiple executions at a time. To develop effective verification and validation mechanisms for confidentiality notions, it is crucial to precisely characterize the requirements of system executions they dictate. In this article, we investigate the relation between abstract non-interference (a weakening of non-interference observing properties of data instead of concrete values) and opacity through the lens of abstract interpretation . By adopting such a holistic, abstract approach, we show how to formally characterize the structure of confidentiality notions and to compare them in terms of the constraints on system executions they impose and verification complexity. In addition, we show how code obfuscation can be restated as a confidentiality problem by defining a corresponding confidentiality notion that can possibly be enforced. Finally, by exploiting the recently proposed static analysis approach for verifying non-interference, based on hypersemantics , we show how to verify abstract non-interference, therefore opacity and other security requirements. Based on abstract interpretation , this yields an effective mechanism to enforce a broad range of confidentiality notions.

Traditional methods for formal verification (FV) of deep neural networks (DNNs) are constrained by a binary encoding of safety properties, where a model is classified as either safe or unsafe (robust or not robust). This binary encoding fails to capture the nuanced safety levels within a model, often resulting in either overly restrictive or too permissive requirements. In this paper, we introduce a novel problem formulation called ABSTRACT DNN-VERIFICATION, which verifies a hierarchical structure of unsafe outputs, providing a more granular analysis of the safety aspect for a given DNN. Crucially, by leveraging abstract interpretation and reasoning about output reachable sets, our approach enables assessing multiple safety levels during the FV process, requiring the same (in the worst case) or even potentially less computational effort than the traditional binary verification approach. Specifically, we demonstrate how this formulation allows rank adversarial inputs according to their abstract safety level violation, offering a more detailed evaluation of the model’s safety and robustness. Our contributions include a theoretical exploration of the relationship between our novel abstract safety formulation and existing approaches that employ abstract interpretation for robustness verification, complexity analysis of the novel problem introduced, and an empirical evaluation considering both a complex deep reinforcement learning task (based on Habitat 3.0) and standard DNN-Verification benchmarks.

Robustness is a key and desirable property of any classifying system, in particular, to avoid the ever-rising threat of adversarial attacks. Informally, a classification system is robust when the result is not affected by the perturbation of the input. This notion has been extensively studied, but little attention has been dedicated to how the perturbation affects the classification. The interference between perturbation and classification can manifest in many different ways, and its understanding is the main contribution of the present article. Starting from a rigorous definition of a standard notion of robustness, we build a formal method for accommodating the required degree of robustness—depending on the amount of error the analyst may accept on the classification result. Our idea is to precisely model this error as an abstraction . This leads us to define weakened forms of robustness also in the context of programming languages, particularly in language-based security, e.g., information-flow policies, and in program verification. The latter is possible by moving from a quantitative (standard) model of perturbation to a novel qualitative model, given by means of the notion of abstraction. As in language-based security, we show that it is possible to confine adversities, which means to characterize the degree of perturbation (and/or the degree of class generalization) for which the classifier may be deemed adequately robust. We conclude with an experimental evaluation of our ideas, showing how weakened forms of robustness apply to state-of-the-art image classifiers.

Dynamic languages, such as JavaScript, employ string-to-code primitives to turn dynamically generated text into executable code at run-time. These features make standard static analysis extremely hard if not impossible, because its essential data structures, i.e., the control-flow graph and the system of recursive equations associated with the program to analyze, are themselves dynamically mutating objects. Nevertheless, assembling code at run-time by manipulating strings, such as by eval in JavaScript, has been always strongly discouraged, since it is often recognized that “ eval is evil ,” leading static analyzers to not consider such statements or ignoring their effects. Unfortunately, the lack of formal approaches to analyze string-to-code statements pose a perfect habitat for malicious code, that is surely evil and do not respect good practice rules, allowing them to hide malicious intents as strings to be converted to code and making static analyses blind to the real malicious aim of the code. Hence, the need to handle string-to-code statements approximating what they can execute, and therefore allowing the analysis to continue (even in the presence of dynamically generated program statements) with an acceptable degree of precision, should be clear. To reach this goal, we propose a static analysis allowing us to collect string values and to soundly over-approximate and analyze the code potentially executed by a string-to-code statement.

Programming language interoperability is the capability of two programming languages to interact as parts of a single system. Each language may be optimized for specific tasks, and a programmer can take advantage of this. HTML, CSS, and JavaScript yield a form of interoperability, working in conjunction to render webpages. Some object oriented languages have interoperability via a virtual machine host (.NET CLI compliant languages in the Common Language Runtime, and JVM compliant languages in the Java Virtual Machine). A high-level language can interact with a lower level one (Apple's Swift and Objective-C). While there has been some research exploring the interoperability mechanisms (Section 1) there is little development of theoretical foundations. This paper presents an approach to interoperability based around theories of equational logic, and categorical semantics. We give ways in which two languages can be blended, and interoperability reasoned about using equations over the blended language. Formally, multi-language equational logic is defined within which one may deduce valid equations starting from a collection of axioms that postulate properties of the combined language. Thus we have the notion of a multi-language theory and much of the paper is devoted to exploring the properties of these theories. This is accomplished by way of category theory, giving us a very general and flexible semantics, and hence a nice collection of models. Classifying categories are constructed, and hence equational theories furnish each categorical model with an internal language; from this we can also establish soundness and completeness. A set-theoretic semantics follows as an instance, itself sound and complete. The categorical semantics is based on some pre-existing research, but we give a presentation that we feel is easier and simpler to work with, improves and mildly extends current research, and in particular is well suited to computer scientists. Throughout the paper we prove some interesting properties of the new semantic machinery. We provide a small running example throughout the paper to illustrate our ideas, and a more complex example in conclusion.

Modern software is no more developed in a single programming language. Instead, programmers tend to exploit cross-language interoperability mechanisms to combine code stemming from different languages, and thus yielding fully-fledged multi-language programs . Whilst this approach enables developers to benefit from the strengths of each single-language, on the other hand it complicates the semantics of such programs. Indeed, the resulting multi-language does not meet any of the semantics of the combined languages. In this paper, we broaden the boundary functions -based approach à la Matthews and Findler to propose an algebraic framework that provides a constructive mathematical notion of multi-language able to determine its semantics . The aim of this work is to overcome the lack of a formal method (resp., model) to design (resp., represent) a multi-language, regardless of the inherent nature of the underlying languages. We show that our construction ensures the uniqueness of the semantic function (i.e., the multi-language semantics induced by the combined languages) by proving the initiality of the term model (i.e., the abstract syntax of the multi-language) in its category.

In recent years, code obfuscation has attracted both researchers and software developers as a useful technique for protecting secret properties of proprietary programs. The idea of code obfuscation is to modify a program, while preserving its functionality, in order to make it more difficult to analyze. Thus, the aim of code obfuscation is to conceal certain properties to an attacker, while revealing its intended behavior. However, a general methodology for deriving an obfuscating transformation from the properties to conceal and reveal is still missing. In this work, we start to address this problem by studying the existence and the characterization of function transformers that minimally or maximally modify a program in order to reveal or conceal a certain property. Based on this general formal framework, we are able to provide a characterization of the maximal obfuscating strategy for transformations concealing a given property while revealing the desired observational behavior. To conclude, we discuss the applicability of the proposed characterization by showing how some common obfuscation techniques can be interpreted in this framework. Moreover, we show how this approach allows us to deeply understand what are the behavioral properties that these transformations conceal, and therefore protect, and which are the ones that they reveal, and therefore disclose.

In this paper we generalize the notion of non-interference making it parametric relatively to what an attacker can analyze about the input/output information flow. The idea is to consider attackers as data-flow analyzers, whose task is to reveal properties of confidential resources by analyzing public ones. This means that no unauthorized flow of information is possible from confidential to public data, relatively to the degree of precision of an attacker. We prove that this notion can be fully specified in standard abstract interpretation framework, making the degree of security of a program a property of its semantics. This provides a comprehensive account of non-interference features for language-based security. We introduce systematic methods for extracting attackers from programs, providing domain-theoretic characterizations of the most precise attackers which cannot violate the security of a given program. These methods allow us both to compare attackers and program secrecy by comparing the corresponding abstractions in the lattice of abstract interpretations, and to design automatic program certification tools for language-based security by abstract interpretation.

Abstract Obfuscation is the art of making code hard to reverse engineer and understand. In this paper, we propose a formal model for specifying and understanding the strength of obfuscating transformations with respect to a given attack model. The idea is to consider the attacker as an abstract interpreter willing to extract information about the program’s semantics. In this scenario, we show that obfuscating code is making the analysis imprecise, namely making the corresponding abstract domain incomplete. It is known that completeness is a property of the abstract domain and the program to analyse. We introduce a framework for transforming abstract domains, i.e., analyses, towards incompleteness. The family of incomplete abstractions for a given program provides a characterisation of the potency of obfuscation employed in that program, i.e., its strength against the attack specified by those abstractions. We show this characterisation for known obfuscating transformations used to inhibit program slicing and automated disassembly.

In the present article, we formally define the notion of abstract program slicing , a general form of program slicing where properties of data are considered instead of their exact value. This approach is applied to a language with numeric and reference values and relies on the notion of abstract dependencies between program statements. The different forms of (backward) abstract slicing are added to an existing formal framework where traditional, nonabstract forms of slicing could be compared. The extended framework allows us to appreciate that abstract slicing is a generalization of traditional slicing, since each form of traditional slicing (dealing with syntactic dependencies) is generalized by a semantic (nonabstract) form of slicing, which is actually equivalent to an abstract form where the identity abstraction is performed on data. Sound algorithms for computing abstract dependencies and a systematic characterization of program slices are provided, which rely on the notion of agreement between program states.

Completeness is a key feature of abstract interpretation. It corresponds to exactness of the abstraction of fix-points and relies upon the need of absence of false alarms in static program analysis. Making abstract interpretation complete is therefore a major problem in approximating the semantics of programming languages. In this paper, we consider the problem of making abstract interpretations complete by minimally modifying the predicate transformer, i.e. the semantics, of a program. We study the mathematical properties of complete functions on complete lattices and prove the existence of minimal transformations of monotone functions to achieve completeness. We then apply minimal complete transformers to prove the minimality of standard program transformations in security, such as static program monitoring.

We introduce a model for mixed syntactic/semantic approximation of programs based on symbolic finite automata (SFA). The edges of SFA are labeled by predicates whose semantics specifies the denotations that are allowed by the edge. We introduce the notion of abstract symbolic finite automaton (ASFA) where approximation is made by abstract interpretation of symbolic finite automata, acting both at syntactic (predicate) and semantic (denotation) level. We investigate in the details how the syntactic and semantic abstractions of SFA relate to each other and contribute to the determination of the recognized language. Then we introduce a family of transformations for simplifying ASFA. We apply this model to prove properties of commonly used tools for similarity analysis of binary executables. Following the structure of their control flow graphs, disassembled binary executables are represented as (concrete) SFA, where states are program points and predicates represent the (possibly infinite) I/O semantics of each basic block in a constraint form. Known tools for binary code analysis are viewed as specific choices of symbolic and semantic abstractions in our framework, making symbolic finite automata and their abstract interpretations a unifying model for comparing and reasoning about soundness and completeness of analyses of low-level code.

How to construct a general program obfuscator? We present a novel approach to automatically generating obfuscated code P2 from any program P whose source code is given. Start with a (program-executing) interpreter interp for the language in which P is written. Then "distort" interp so it is still correct, but its specialization P2 w.r.t. P is transformed code that is equivalent to the original program, but harder to understand or analyze. Potency of the obfuscator is proved with respect to a general model of the attacker, modeled as an approximate (abstract) interpreter. A systematic approach to distortion is to make program P obscure by transforming it to P2 on which (abstract) interpretation is incomplete. Interpreter distortion can be done by making residual in the specialization process sufficiently many interpreter operations to defeat an attacker in extracting sensible information from transformed code. Our method is applied to: code flattening, data-type obfuscation, and opaque predicate insertion. The technique is language independent and can be exploited for designing obfuscating compilers.

Reliable and secure system design requires an increasing number of methods, algorithms, and tools for automatic program manipulation. Any program change corresponds to a transformation that affects the semantics at some given level of abstraction. We call these techniques model deformations. In this paper we propose a mathematical foundation for completeness-driven deformations of transition systems w.r.t. a given abstraction, and we introduce an algorithm for systematic deformation of Kripke structures for inducing strong preservation in abstract model checking. We prove that our model deformations are deeply related with must and may transitions in modal transition systems.

This paper explores a three dimensional characterisation of a declassification-based non-interference policy and its consequences. Two of the dimensions consist of specifying: (a) the power of the attacker, that is, what public information a program has that an attacker can observe; and (b) what secret information a program has that needs to be protected. Both these dimensions are regulated by the third dimension: (c) the choice of program semantics, for example, trace semantics or denotational semantics, or any semantics in Cousot's semantics hierarchy. To check whether a program satisfies a non-interference policy, one can compute an abstract domain that over-approximates the information released by the policy and then check whether program execution can release more information than permitted by the policy. Counterexamples to a policy can be generated by using a variant of the Paige–Tarjan algorithm for partition refinement. Given the counterexamples, the policy can be refined so that the least amount of confidential information required for making the program secure is declassified.

Completeness in abstract interpretation models the ideal situation where no loss of precision is introduced in computations by approximating concrete data by their abstractions. If we interpret the abstraction as the ability of an attacker to distinguish, i.e., observe, properties of public computations, and the computation as the concrete denotational semantics of the program, then the lack of precision, encoded in abstract interpretation as a lack of completeness, corresponds precisely to the leakage of information corresponding to a violated security policy. This correspondence allows us to inherit, in the field of language-based security, the whole theory and methodology for making abstract domains complete. In particular, we prove that an adjoint relation exists between the power of the attacker and the amount of the information released – the more the attacker can observe, the less information can be kept private. This characterisation is achieved by interpreting, in the security context, the standard adjoint transformations making an abstract domain complete by refining and simplifying abstractions.

Questo rapporto è disponibile su Web all’indirizzo: This report is available on the web at the address:

We discuss the relation between program slicing and data dependencies. We claim that slicing can be defined, and therefore calculated, parametrically on the chosen notion of dependency, which implies a different result when building the program dependency graph. In this framework, it is possible to choose dependency in the syntactic or semantic sense, thus leading to compute possibly different, smaller slices. Moreover, the notion of abstract dependency, based on properties instead of exact data values, is investigated in its theoretical meaning. Constructive ideas are given to compute abstract dependencies on expressions, and to transform properties in order to rule out some dependencies. The application of these ideas to information flow is also discussed.

In this paper we study the connection between the structure of relational abstract domains for program analysis and compositionality of the underlying semantics. Both can be systematically designed as solution of the same abstract domain equation involving the same domain refinement: the reduced power operation. We prove that most well-known compositional semantics of imperative programs, such as the standard denotational and weakest precondition semantics can be systematically derived as solutions of simple abstract domain equations. This provides an equational presentation of both semantics and abstract domains for program analysis in a unique formal setting. Moreover both finite and transfinite compositional semantics share the same structure, and this allows us to provide consistent models for program manipulation. Categories and Subject Descriptors D.3 [Programming languages]: Formal definitions and theory---Semantics; F.3 [Logics and meanings of programs ]: Semantics of Programming Languages---algebraic approaches to semantics, denotational semantics, operational semantics General Terms Theory, Verification Keywords Abstract interpretation, reduced power, compositional semantics, transfinite semantics, program manipulation. 1.

We characterize the symmetric structure of Cousot's hierarchy of semantics in terms of a purely algebraic manipulation of abstract domains. We consider domain complementation in abstract interpretation as a formal method for systematically deriving complementary semantics of programming languages. We prove that under suitable hypothesis the semantics abstraction commutes with respect to domain complementation. This result allows us to prove that angelic and demonic/innite semantics are complementary and provide a minimal decomposition of all natural-style trace-based, relational, denotational, Dijkstra's predicate transformer and Hoare's axiomatic semantics. We apply this construction to the case of concurrent constraint programming, characterizing well known semantics as abstract interpretation of maximal traces of constraints. Categories and Subject Descriptors D.3 [Programming languages]: Formal denitions and theory|Semantics; F.3 [Logics and meanings of programs ]: Semantics of...