Markus Roggenbach

Tonicha Crook, Jay Morgan, Arno Pauly et al.

There is a strong consensus that combining the versatility of machine learning with the assurances given by formal verification is highly desirable. It is much less clear what verified machine learning should mean exactly. We consider this question from the (unexpected?) perspective of computable analysis. This allows us to define the computational tasks underlying verified ML in a model-agnostic way, and show that they are in principle computable.

Tobias Rosenberger, Saddek Bensalem, Alexander Knapp et al.

This paper provides the first correct semantical representation of UML state-machines within the logical framework of an institution (previous attempts were flawed). A novel encoding of this representation into first-order logic enables symbolic analyses through a multitude of theorem-provers. UML state-machines are central to model-based systems-engineering. Till now, state-machine analysis has been mostly restricted to model checking, which for state-machines suffers heavily from the state-space explosion problem. Symbolic reasoning, as enabled and demonstrated here, provides a powerful alternative, which can deal with large or even infinite state spaces. Full proofs are given.

Antonio Cerone, Markus Roggenbach, James Davenport et al.

This white paper argues that formal methods need to be better rooted in higher education curricula for computer science and software engineering programmes of study. To this end, it advocates (i) improved teaching of formal methods; (ii) systematic highlighting of formal methods within existing, `classical' computer science courses; and (iii) the inclusion of a compulsory formal methods course in computer science and software engineering curricula. These recommendations are based on the observations that (a) formal methods are an essential and cost-effective means to increase software quality; however (b) computer science and software engineering programmes typically fail to provide adequate training in formal methods; and thus (c) there is a lack of computer science graduates who are qualified to apply formal methods in industry. This white paper is the result of a collective effort by authors and participants of the 1st International Workshop on "Formal Methods, Fun for Everybody" which was held in Bergen, Norway, 2-3 December 2019. As such, it represents insights based on learning and teaching computer science and software engineering (with or without formal methods) at various universities across Europe.

Irina Mariuca Asavoae, Hoang Nga Nguyen, Markus Roggenbach et al.

In this position paper we advocate software model checking as a technique suitable for security analysis of mobile apps. Our recommendation is based on promising results that we achieved on analysing app collusion in the context of the Android operating system. Broadly speaking, app collusion appears when, in performing a threat, several apps are working together, i.e., they exchange information which they could not obtain on their own. In this context, we developed the Kandroid tool, which provides an encoding of the Android/Smali code semantics within the K framework. Kandroid allows for software model checking of Android APK files. Though our experience so far is limited to collusion, we believe the approach to be applicable to further security properties as well as other mobile operating systems.

Jorge Blasco, Thomas M. Chen, Igor Muttik et al.

Android is designed with a number of built-in security features such as app sandboxing and permission-based access controls. Android supports multiple communication methods for apps to cooperate. This creates a security risk of app collusion. For instance, a sandboxed app with permission to access sensitive data might leak that data to another sandboxed app with access to the internet. In this paper, we present a method to detect potential collusion between apps. First, we extract from apps all information about their accesses to protected resources and communications. Then we identify sets of apps that might be colluding by using rules in first order logic codified in Prolog. After these, more computationally demanding approaches like taint analysis can focus on the identified sets that show collusion potential. This "filtering" approach is validated against a dataset of manually crafted colluding apps. We also demonstrate that our tool scales by running it on a set of more than 50,000 apps collected in the wild. Our tool allowed us to detect a large set of real apps that used collusion as a synchronization method to maximize the effects of a payload that was injected into all of them via the same SDK.

Irina Mariuca Asavoae, Jorge Blasco, Thomas M. Chen et al.

Android OS supports multiple communication methods between apps. This opens the possibility to carry out threats in a collaborative fashion, c.f. the Soundcomber example from 2011. In this paper we provide a concise definition of collusion and report on a number of automated detection approaches, developed in co-operation with Intel Security.

Alexander Knapp, Till Mossakowski, Markus Roggenbach et al.

We present an institution for UML state machines without hierarchical states. The interaction with UML class diagrams is handled via institutions for guards and actions, which provide dynamic components of states (such as valuations of attributes) but abstract away from details of class diagrams. We also study a notion of interleaving product, which captures the interaction of several state machines. The interleaving product construction is the basis for a semantics of composite structure diagrams, which can be used to specify the interaction of state machines. This work is part of a larger effort to build a framework for formal software development with UML, based on a heterogeneous approach using institutions.

Alexander Knapp, Till Mossakowski, Markus Roggenbach

We present a framework for formal software development with UML. In contrast to previous approaches that equip UML with a formal semantics, we follow an institution based heterogeneous approach. This can express suitable formal semantics of the different UML diagram types directly, without the need to map everything to one specific formalism (let it be first-order logic or graph grammars). We show how different aspects of the formal development process can be coherently formalised, ranging from requirements over design and Hoare-style conditions on code to the implementation itself. The framework can be used to verify consistency of different UML diagrams both horizontally (e.g., consistency among various requirements) as well as vertically (e.g., correctness of design or implementation w.r.t. the requirements).

Phillip James, Markus Roggenbach

The development and application of formal methods is a long standing research topic within the field of computer science. One particular challenge that remains is the uptake of formal methods into industrial practices. This paper introduces a methodology for developing domain specific languages for modelling and verification to aid in the uptake of formal methods within industry. It illustrates the successful application of this methodology within the railway domain. The presented methodology addresses issues surrounding faithful modelling, scalability of verification and accessibility to modelling and verification processes for practitioners within the domain.