Software and security

Software and Security at SIT

Prof. Bertrand Meyer
Prof. Bertrand Meyer

Head of the Chair of Software and Security at the Schaffhausen Institute of Technology

Professor of Software Engineering (emeritus) at ETH Zurich: Chair of Software Engineering. Chief Technology Officer, Eiffel Software.

CV: Électricité de France 1974-1983; Univ. of California Santa Barbara 1983-1985; Eiffel Software, Santa Barbara since 1985 (president until 2001, then CTO); ETH Zurich since Oct. 2001 (department chair 2004-2006).

What is the Software Analysis Theory?

Modern software systems are extremely complex constructions. Some of them are more complex than any engineering system (jet plane, space station, airport...) ever built by humankind.

In fact, their level of complexity is more comparable to that of human systems such as a large city, but with a major difference: in a human system, many things can go wrong without shutting down the system. For example, in any city at any given time, there are traffic jams, accidents, closed streets, burglaries and so on, which cause disruption but not shutdown. In a software system, everything has to be right (changing a single bit in the object code of Windows, out of billions, may render the OS inoperative). Conversely, it is possible to make major changes that are not immediately detected; intruders take advantage of this property.

Fortunately, techniques of software analysis, which treat a software system as an artifact worthy of large-scale extensive study (with both logical techniques and big-data/machine learning techniques) have made tremendous progress in recent years.

The Software Analysis Factory is a general platform combining many different techniques to dissect software systems, small, large, or very large, and explore their properties.

A SAF user feeds a software system (source form and object form) into the SAF and also presents a number of questions ("is a buffer overflow possible?"); the SAF produces responses in the form of an analysis. The key is the extremely high quality of such analyses, which must be sound (give correct answers) and precise (give the best answers), as well as fast. This quality, relying on advanced techniques (abstract interpretation, model checking, static analysis) is the first unique feature of the SAF.

The term "query" will denote a type of analysis (a type of question, such as buffer overflow).

The second key distinctive characteristic of the SAF is its parameterizability. The above-simplified API is the user API. The second API, giving the SAF its "universal" nature, is the technology API.

Since software analysis is fundamentally dependent on the input format (e.g. programming language), this API provides a way to make the SAF able to handle such a format. The term "handle" will denote such an adaptation (the Python handle, the .NET handle, etc.)

The role of formalism in system requirements

Jean-Michel Bruel, Sophie Ebersold, Florian Galinier, Manuel Mazarra, Alexander Naumchev, Bertrand Meyer.

ACM Computing Surveys, 2021 (accepted for publication).

Mechanically-checked soundness of type-based null safety

Alexander Kogtenkov

CPP 2021 Lightning Talks (POPL 2021), 2021–01–18.

Making null safety formalization correct

Alexander Kogtenkov

SITSOFT Software engineering seminar, 2021–10–06.

Type-based deadlock prevention in SCOOP

Concurrent programming introduces new challenges for developers due to race conditions, deadlocks, starvation, and priority inversion. Structured concurrent object-oriented programming (SCOOP) is data-race-free but does not guarantee deadlock freedom. The goal of this project is to provide a sound solution to the problem using static analysis and replacing exact modeling of object structure at run-time with an approximation based on type information. The project includes the development of the rules that guarantee deadlock freedom, their implementation and assessment on an existing code base, a (preferably, mechanically checked) formal proof of the technique.

Supervisor: Alexander Kogtenkov

Verification of programming languages specifications

Some programming languages are specified by text documents describing their syntax and semantics. The goal of the project is to develop a model of the programming language specification, to define the requirements that this model should satisfy, and to apply them to real-world specifications. Examples of the requirements include "all terminal symbols should be defined and used", "definitions should not be circular", "dynamic semantics should cover all cases described by static semantics", etc. Warning: most contemporary language specifications are huge, therefore, converting them to a format usable for formal verification might be time-consuming, so, please, apply to this project only if you are confident that you would be able to cover at least one currently used programming language specification.

Supervisor: Alexander Kogtenkov, Bertrand Meyer

Design by contract in dynamic context

The method of "Design by Contract" is well-studied and understood for static relations in OOP languages. In particular, it defines how to compute preconditions and postconditions for methods in descendant classes. But what if a method is used to initialize a closure variable (aka function pointer, delegate, agent, etc.) and this closure needs to have a non-trivial precondition or postcondition? The goal of the project is to develop a model for such reattachment, to specify evaluation and responsibility rules for assertions in these conditions, to provide a prototype implementation, and to prove the soundness of the model.

Supervisor: Alexander Kogtenkov

Client-side selection of repeatedly-inherited methods

Multiple inheritances of implementation in an object-oriented programming language have an issue with repeated inheritance when the same parent method can have more than one implementation in a particular descendant (so-called "diamond problem"). In order to support dynamic dispatch to an intended method, one of the implementations needs to be selected. This can be done at the supplier side (e.g., using the "select" adaptation clause in Eiffel), but fixes the selection once and for all. An alternative is to do the selection at the client-side. Provided that the replicated methods can come in groups rather than alone, the selection should be parent-class-based instead of method-based. At least 2 projects are possible here. The common goal of either project is to develop a mechanism to select the required parent at the client-side. Then, the specific goal of one project is to formally describe the semantics of the mechanism, and to prove that it has certain properties (e.g., preserves object identity, preserves parent semantics, is type-safe, etc.). The specific goal of another project is to develop an efficient implementation of the mechanism and to prove that this implementation satisfies the expected behavior.

Supervisor: Alexander Kogtenkov

Safe covariance of argument types

Argument type covariance is essential to support the approach of "Design by Contract" in object-oriented programming languages. However, its combination with polymorphism and dynamic dispatch is known to be type-unsafe. One solution to this problem is to disable one of the variability dimensions in every particular case. This is achieved by introducing type annotations that restrict type compatibility. The goal of the project is to formalize the rules of the corresponding type system, and to prove its soundness.

Supervisor: Alexander Kogtenkov

Verified object-oriented programming language compiler

Top-level universities have developed mechanically verified compilers for subsets of C (CompCert) and ML (CakeML). The goal of the project is to bring an object-oriented language to the scene of formally verified compilers. Given that this is an ambitious target with potentially several Ph.D. theses for a non-trivial OO language, for a master's thesis, a very limited subset of an object-oriented language would be considered, using C or ML as a backend to rely on one of the existing verified frameworks.

Supervisor: Alexander Kogtenkov

Formal verification of string constraints for Eiffel programs

Formal verification is essential to improve software quality and provide a high level of assurance of software correctness. To formally verify Eiffel programs, the semantics of the programs is formally specified in mathematical formalisms (i.e., logical formulas), which can be fed into mechanical verification tools (e.g., SMT solvers) to perform rigorous analysis on the specifications. This project aims to provide the support for formal analysis of string constraints for string-manipulation programs, i.e., Eiffel program: A set of mapping rules should be proposed to translate Eiffel strings into Boogie strings that are verifiable by SMT solvers. An automatic translation should be implemented to facilitate the translation. Verification of string constraints (e.g., word equations, length constraints, and regular membership queries) for Eiffel programs should be performed based on the proposed translation-based approach.

Supervisor: Li Huang

Verification tool fundamental correctness

Program verification relies on the program state invariants and on the rules to translate an input program and its specification into formulas describing program state updates, subsequently generating verification conditions to be checked by an SMT solver. Incorrect invariants or translation rules can lead to contradictions interpreted as successful verification of the program, making the verifier useless. The goal of the project is to demonstrate soundness and consistency of the axioms and translation rules used in AutoProof - a state-of-the-art verifier of object-oriented programs.

Supervisor: Alexander Kogtenkov

Bringing AutoProof to the cloud

AutoProof is an advanced verification technology that makes it possible to mathematically and fully automatically prove correctness of Eiffel programs against requirements specified as code contracts. AutoProof currently exists as a cross-platform desktop application that supports graphical and command-line modes of execution. The next step, which is the idea of this thesis project, is to bring AutoProof to the cloud. The market of cloud IDEs is rapidly growing, and the project will start with exploring the available open source solutions. The next step would be to choose one and tailor it to support Eiffel and AutoProof.

Supervisor: Alexandr Naumchev

Establishing a software process for AutoProof

The AutoProof verification system, originally developed at ETH Zurich and now at SIT, provides a powerful environment for proving the correctness of contract-equipped object-oriented programs. The goal of the project is to set up a proper professional-quality process for the current and future development process, with such elements as: commit-to-review (CTR) scheme; bug reporting and tracking; regression test suite and process for automatically running; build and configuration scripts for using AutoProof on various platforms; integration with EiffelStudio development.

Supervisor: Bertrand Meyer, Alexandr Naumchev

Making AutoProof verification incremental

Formal verification is time-consuming because the underlying tools (like SMT solvers) do not provide any guarantees on the time required to confirm or refute a proof goal. This bans inclusion of the verifier in the development cycle based on frequent (or background) compilation. Real-life software development usually relies on incremental changes, each affecting just a small portion of code. For modular verifiers, such as AutoProof, the incremental nature of software development opens the possibility to re-verify only the modified parts instead of performing verification from scratch. The project goal is to design, develop, and integrate such an incremental verification mechanism, and demonstrate its practical usefulness on the existing code base.

Supervisor: Alexander Kogtenkov

Here you can find the most recent mentions and news about the Chair.

Interested in research with Prof. Bertrand Meyer?

Apply now for your PhD or postdoc research.