Malware analysis represents a difficult task due to its ever-changing nature, where attackers invent new techniques for avoiding or counter-attacking analysis and prevention mechanisms. During fast-response investigations, a vital element is extracting or checking information, in order to take proper action. One key aspect that is currently missing, in a general sense, is a system which security researchers can query in order to obtain a quick verdict about the capabilities of a malware. The proposed solution is a framework for formal analysis of applications’ behavior, called Formal Tainting-Based Framework, that uses a combination of binary instrumentation, taint analysis, and runtime verification in order to selectively extract behavioral properties of a malware. These are then formalized in order to check if the application expresses certain capabilities. The formal aspect also represents a significant contribution, as we introduce a specific temporal logic, which overcomes obstacles for expressing program events. The findings are accompanied by a concrete implementation, which proved effective and efficient against real-life malware, as highlighted by an evaluation. Furthermore, the framework has been evaluated in realistic cyber forensics scenarios, demonstrating its potential to assist security researchers by reducing analysis time and effort.

Python’s typing system has evolved pragmatically into a powerful but theoretically fragmented system, with scattered specifications. This paper proposes a formalization to address this fragmentation. The central contribution is a formal foundation that uses existential types to elegantly describe Python’s type system. This work aims to serve as a fundamental first step towards the future development of type inference tools.

Initial algebra semantics provides a generic and principled framework to study induction. In this paper, we give a complete formalization of ini- tial algebra semantics and inductive reasoning using matching logic—a small and unifying logic for formal semantics of programming languages. Specifi- cally, we define initial algebra semantics as matching logic theories and derive induction/iteration/primitive-recursion principles as formal theorems within matching logic, using its proof system. This way, we obtain, for the first time, a rigorous logical foundation for general initial algebra semantics and induc- tion, both proof-theoretically and model-theoretically. As a bonus, matching logic admits the smallest known proof checker for a logic supporting inductive proofs, of only 240 lines of code.

The Multiple Traveling Salesman Problem (multiple-TSP) is a straightforward extension of the well-known Traveling Salesman Problem (TSP), in which more salesmen must visit a set of interconnected cities. Ant Colony Optimization (ACO) algorithms are designed to build sequentially the solutions, aspect which on multiple-TSP imposes new challenges. Compared to TSP which deals with one sample space - the set of cities (locations), multiple-TSP involves two sample spaces: the set of salesmen (agents) and the set of cities. Existing ACO algorithms addressing multiple-TSP are two-phase sampling procedures which, firstly, independently sample from the first set (the set of salesmen), and then conditionally sample from the second set. Our claim is that a joint sampling mechanism, which will exploit a joint probability space, is likely to lead to superior results. We validate our hypothesis by implementing five ACO-based algorithms to solve multiple-TSP: three of them are two-phase algorithms exploring various methods to sample from the salesmen space, while two of them implement the joint sampling scheme. The results are analyzed both in a single-objective manner that considers the minimization of the longest tour, and also from a bi-objective perspective that considers two conflicting objectives: 1) minimization of the total traveled distance and 2) work balancing – which amounts to minimizing the amplitude of the costs of individual tours.

Software engineers want to be real engineers.Real engineers use mathematics.Formal methods are the mathematics of software engineering.Therefore, software engineers should use formal methods."Mike HollowayThe Working Formal Methods Symposium (FROM) aims to bring together researchers and practitioners who work on formal methods by contributing new theoretical results, methods, techniques, and frameworks, and/or make the formal methods to work by creating or using software tools that apply theoretical contributions.FROM

This special issue marks the 60th birthday of Professor Gabriel Ciobanu.It consists of 7 original contributions from colleagues who have accompanied Gabriel through his scientific life in one way or another, be it in joint projects, research articles, or even the writing of complete books.We would like to thank all the contributors to this special issue for their hard work and

Abstract Two programs are fully equivalent if, for the same input, either they both diverge or they both terminate with the same result. Full equivalence is an adequate notion of equivalence for programs written in deterministic languages. It is useful in many contexts, such as capturing the correctness of program transformations within the same language, or capturing the correctness of compilers between two different languages. In this paper we introduce a language-independent proof system for full equivalence, which is parametric in the operational semantics of two languages and in a state-similarity relation. The proof system is sound: a proof tree establishes the full equivalence of the programs given to it as input. We illustrate it on two programs in two different languages (an imperative one and a functional one), that both compute the Collatz sequence. The Collatz sequence is an interesting case study since it is not known whether the sequence terminates or not; nevertheless, our proof system shows that the two programs are fully equivalent (even if we cannot establish termination or divergence of either one).

Abstract We propose a logic and a deductive system for stating and automatically proving the equivalence of programs written in languages having a rewriting-based operational semantics. The chosen equivalence is parametric in a so-called observation relation, and it says that two programs satisfying the observation relation will inevitably be, in the future, in the observation relation again. This notion of equivalence generalises several well-known equivalences and is appropriate for deterministic (or, at least, for confluent) programs. The deductive system is circular in nature and is proved sound and weakly complete; together, these results say that, when it terminates, our system correctly solves the given program-equivalence problem. We show that our approach is suitable for proving equivalence for terminating and non-terminating programs as well as for concrete and symbolic programs. The latter are programs in which some statements or expressions are symbolic variables. By proving the equivalence between symbolic programs, one proves the equivalence of (infinitely) many concrete programs obtained by replacing the variables by concrete statements or expressions. The approach is illustrated by proving program equivalence in two languages from different programming paradigms. The examples in the paper, as well as other examples, can be checked using an online tool.