ABSTRACT. The safety and correctness of of avionics software products is paramount, especially for safety-critical software. It is thus developed against stringent international regulations (DO-178). Nonetheless, the size and complexity of avionics software products have grown exponentially in the four last decades. Legacy methods, based on informal designs, testing and intellectual analysis, have been shown to scale poorly, as opposed to some formal techniques. Airbus have therefore been transforming the development processes of avionics software, taking advantage from sound formal formal methods to preserve safety, while improving cost-efficiency. The talk will report on this transformation.

ABSTRACT. This work demonstrates how highly automated theorem proving can be leveraged for sparing testing costs during certification of safety-critical software such as in avionics. A verification framework for distributed interactive systems is presented. Components are modeled as stream processing functions. The functional methodology is modular with respect to serial, parallel and feedback composition. To specify and formally verify properties of distributed systems, a stream-based verification infrastructure is encoded in the theorem prover Isabelle. Composition operators for components are provided, thus allowing to scale proofs from individual components to complex networks. The underlying mathematical theory FOCUS stands out among competitors by the fact that refinement is fully compositional. The associativity and commutativity of the provided general composition operator enables a compositional verication. In this paper the stream theory encoded in Isabelle is demonstrated. This represents a small part of our encoding of the methodology focusing only on channel histories specications, yet sufficient to demonstrate dealing successfully with underspecification, supporting automatic refinement checking during design time, time-sensitive specication, as well as verifying safety and liveness properties. The theory is evaluated in a case study where the occurring refinement steps from system requirements, to high level requirements, to low level requirements, until an implementation is reached, are demonstrated to be proven correct at the push of a button.

ABSTRACT. Backward symbolic execution (BSE), also known as weakest precondition computation, is a useful technique to determine validity of assertions in program code by transforming its semantics into boolean conditions for an SMT solver. Regrettably, the literature does not cover various challenges which arise during its implementation, especially when we want to reason about heap objects using the theory of arrays and to use the SMT solver efficiently. In this paper, we present our achievements in this area. Our contribution is threefold. First, we summarize the two most popular state-of-the-art approaches used for BSE, denoting them as disjunct propagation and conjunct combination. Second, we present a novel method for modelling heap operations in BSE using the theory of arrays, optimized for incremental checking during the analysis and handling the input heap. Third, we compare both approaches with our heap handling implementation on a set of program examples, presenting their strengths and weaknesses. The evaluation shows that conjunct combination is the most efficient variant, exceeding the straightforward implementation of disjunct propagation in an order of magnitude.

ABSTRACT. According to security rankings such as the SANS Top 25 and the OWASP Top 10, access-control vulnerabilities are still highly relevant. Even though developers use web frameworks such as Spring and Struts, which handle the entire access-control mechanism, their implementation can still be vulnerable because of misuses, errors, or inconsistent implementation from the design specification. We propose AuthCheck, a static analysis that tracks the program’s state using a finite state machine to report illegal states caused by vulnerable implementation. We implemented AuthCheck for the Spring framework and identified four types of mistakes that developers can make when using Spring Security. With AuthCheck, we analyzed an existing open-source Spring application with inserted vulnerable code and detected detected the vulnerabilities.

ABSTRACT. In this paper, we present fkcc, a scripting tool to prototype program analyses and transformations exploiting the affine form of Farkas lemma. Our language is general enough to prototype in a few lines sophisticated termination and scheduling algorithms. The tool is freely available and may be tried online via a web interface. We believe that fkcc is the missing chain to accelerate the development of program analyses and transformations exploiting the affine form of Farkas lemma.

ABSTRACT. The Abstract Interpretation framework provides invaluable guidance for the design of abstract domains to be used in static analysis tools. Nonetheless, the development of an adequate abstract domain can be a challenging task: besides the mandatory correctness requirements, also its precision and efficiency need to be properly considered. Drawing mainly from past experience, we show a few examples of the problems that an abstract domain developer may be facing. We rediscuss the tradeoffs that could be adopted while working through the solutions, somehow confirming known rules of thumb, possible exceptions to the rules of thumb and other interesting relationships between correctness, precision and efficiency.

ABSTRACT. Safety-critical embedded software has to satisfy stringent quality requirements. For example, one such requirement, imposed by the relevant safety standard (ISO26262), is that no critical run-time errors must occur. In the last years, we introduced sound static analysis methods and tools in the development process for large-scale software with several million lines of code. They are used to prove highly automated the absence of run-time errors – especially caused by integration. The talk will report on this experience and give an outlook about future challenges.

ABSTRACT. Context-sensitive global analysis of large code bases can be expensive, sometimes making impractical its use "on-line" during software development. However, often program modifications are small and isolated within a few components, which makes it desirable to reuse as much as possible previous analysis results. In CiaoPP incrementality-based cost reductions have been achieved in context-sensitive analysis through two separate techniques: modular analysis and fine grain incremental analysis. We have recently been working on combining these two techniques in order to achieve incrementality at both the intra- and inter-modular levels. Our objective is to give an overview (and demo) of the approach and, specially, report on the results obtained so far. The preliminary results show that the modular incremental algorithm achieves competitive and, in some cases, improved performance when compared to the non-modular, fine-grain incremental analysis, and outperforms traditional modular analysis even when analyzing from scratch.

ABSTRACT. Software model checking has experienced significant progress in the last two decades, however, one of its major bottlenecks for practical applications remains its scalability and adaptability. Here, we describe an approach to integrate software model checking techniques into the DevOps culture by exploiting practices such as continuous integration and regression tests. In particular, our proposed approach looks at the modifications to the software system since its last verification, and submits them to a continuous formal verification process, guided by a set of regression test cases. Our vision is to focus on the developer in order to integrate formal verification techniques into the developer workflow by using their main software development methodologies and tools.

ABSTRACT. We present PrideMM, an efficient model checker for second-order logic enabled by recent breakthroughs in quantified satisfiability solvers. We argue that second-order logic sits at a sweet spot: constrained enough to enable practical solving, yet expressive enough to cover an important class of problems not amenable to (non-quantified) satisfiability solvers. To the best of our knowledge PrideMM is the first automated model checker for second-order logic formulae.

We demonstrate the usefulness of PrideMM by applying it to problems drawn from recent work on memory specifications, which define the allowed executions of concurrent programs. For traditional memory specifications, program executions can be evaluated using a satisfiability solver or using equally powerful ad hoc techniques. However, such techniques are insufficient for handling some emerging memory specifications.

We evaluate PrideMM by implementing a variety of memory specifications, including one that cannot be handled by satisfiability solvers. In this problem domain, PrideMM provides usable automation, enabling a modify-execute-evaluate pattern of development where previously manual proof was required.