Education: Lipari Summer School on Abstract Interpretation 2024
Lipari, Italy, September 1-7, 2024
Patrick Cousot started the summer school introducing the basic concepts necessary to define the semantics of programs (i.e. in rule-based and the fixpoint form), program properties and the best abstraction of properties in an abstract domain. Afterwards, Cousot showed that the theory of program logics are the best abstractions of their semantics and they can be expressed as fixpoints. Then, he studied the correspondence between fixpoints and proof systems. This studio allows us to design sound and complete proof rules by calculus using fixpoint induction.
Enea Zaffanella talked about the widening and narrowing operators in static analysis based on abstract interpretation. He started the talk explaining the definition and the significance of widening operators, and continued with practical examples of analysis, such as interval analysis, demonstrating how variables can be mapped to integer intervals and how operators on these intervals can provide correct approximations of concrete operations. Lastly, Zaffanella emphasized that the correctness of abstract operators must be ensured to guarantee the validity and utility of the analysis in practice.
Thomas Jensen discussed “Software Security and Abstract Interpretation”, in particular he talked about the security in software and the using of Abstract Interpretation to analyze and improve the security in softwares. Jensen started addressing the main properties of information security: confidentiality, integrity, and availability. Confidentiality refers to the protection of information from unauthorized access; integrity, to ensuring that data is accurate and not altered by external entities; and availability, to the ability to access data and services when needed. Subsequently, he examined various software security threats, including viruses, worms, ransomware, encryption misuse issues, and security challenges for operating systems. He suggested several techniques to improve software security, such as secure programming, code verification through static and dynamic analysis, and the use of programming languages designed with security in mind. A central point of the speech is abstract interpretation. Used with static analysis, it allows to obtain approximate but correct predictions about the behavior of the software, and it is particularly useful in identifying vulnerabilities such as buffer overflows or problems related to the security of the control flow.
Helmut Seidl’s talk was focused on numerical abstract domains in static analysis. Seidl discussed the foundational ingredients of static analysis, illustrating them through simple code examples. He highlighted the importance of various abstract domains, such as interval abstraction, octagon abstraction, and polyhedral abstraction, and posed the question of which abstraction to choose, noting that a more precise domain may incur higher computational costs.
Laurent Mauborgne discussed the use of the Abstract Interpretation in the industry, in particular he explained why it is important to guarantee software security in critical embedded systems such as those in the aerospace, automotive and railway industries. A central theme is the importance of ensuring that real-time systems respect stringent timing constraints to avoid failures. He explored the problem of computing the Worst Case Execution Time (WCET), describing the difficulties related to the dependence of the machine state and the size of the state space. Mauborgne also explored interference problems in multi-core systems, where shared resources such as memory and caches can introduce delays and instabilities.
Caterina Urban talked about the formal methods for machine learning pipelines. She highlighted the critical role of machine learning (ML) in high-stakes applications, emphasizing the need for correctness guarantees in ML systems. Urban also discussed several notable incidents, such as self-driving cars and healthcare applications, where failures in ML models have led to serious consequences. Then, she introduced formal methods, such as deductive verification and model checking, as tools to analyze and verify the correctness of ML models. The latter part of her speech was focused on static analysis methods for verifying properties of ML models, particularly through forward analysis: she explained how these methods can help to ensure that the outputs of ML models remain stable under small input perturbations, thus enhancing the reliability of predictions.
Luca Negrini presented LiSA (Library for Static Analysis), a Java library designed to build static analyzers based on Abstract Interpretation theory. He started describing the architecture of LiSA from a high-level and secondly he showed some live-coding tutorials.
Laura Titolo ended the summer school presenting her work at NASA, in particular she talked about the floating-point errors in avionics applications at NASA. She began by discussing the importance of formal methods in NASA’s Verification and Validation (V&V) processes. The key topic of the presentation was the challenge posed by floating-point round-off errors. In IT, floating-point arithmetic involves approximations of real numbers, which can lead to errors when computations are rounded. This becomes critical in safety-critical systems like avionics, where small errors can accumulate and cause significant deviations from expected results (e.g. Ariane V). At the end, Titolo introduced PRECiSA, a static analysis tool developed by NASA that automatically estimates round-off errors in floating-point programs.
