Dilian Gurov

Predrag Filipovikj, Dilian Gurov, Mattias Nyberg

Stateflow models are complex software models, often used as part of safety-critical software solutions designed with Matlab Simulink. They incorporate design principles that are typically very hard to verify formally. In particular, the standard exhaustive formal verification techniques are unlikely to scale well for the complex designs that are developed in industry. Furthermore, the Stateflow language lacks a formal semantics, which additionally hinders the formal analysis. To address these challenges, we lay here the foundations of a scalable technique for provably correct formal analysis of Stateflow models, with respect to invariant properties, based on bounded model checking (BMC) over symbolic executions. The crux of our technique is: i) a representation of the state space of Stateflow models as a symbolic transition system (STS) over the symbolic configurations of the model, as the basis for BMC, and ii) application of incremental BMC, to generate verification results after each unrolling of the next-state relation of the transition system. To this end, we develop a symbolic structural operational semantics (SSOS) for Stateflow, starting from an existing structural operational semantics (SOS), and show the preservation of invariant properties between the two. Next, we define bounded invariant checking for STS over symbolic configurations as a satisfiability problem. We develop an automated procedure for generating the initial and next-state predicates of the STS, and propose an encoding scheme of the bounded invariant checking problem as a set of constraints, ready for automated analysis with standard, off-the-shelf satisfiability solvers. Finally, we present preliminary performance results by applying our tool on an illustrative example.

Mojtaba Eshghie, Cyrille Artho, Dilian Gurov

In this work we propose Dynamit, a monitoring framework to detect reentrancy vulnerabilities in Ethereum smart contracts. The novelty of our framework is that it relies only on transaction metadata and balance data from the blockchain system; our approach requires no domain knowledge, code instrumentation, or special execution environment. Dynamit extracts features from transaction data and uses a machine learning model to classify transactions as benign or harmful. Therefore, not only can we find the contracts that are vulnerable to reentrancy attacks, but we also get an execution trace that reproduces the attack.

Marieke Huisman, Dilian Gurov, Alexander Malkis

For many decades, formal methods are considered to be the way forward to help the software industry to make more reliable and trustworthy software. However, despite this strong belief and many individual success stories, no real change in industrial software development seems to be occurring. In fact, the software industry itself is moving forward rapidly, and the gap between what formal methods can achieve and the daily software-development practice does not appear to be getting smaller (and might even be growing). In the past, many recommendations have already been made on how to develop formal-methods research in order to close this gap. This paper investigates why the gap nevertheless still exists and provides its own recommendations on what can be done by the formal-methods-research community to bridge it. Our recommendations do not focus on open research questions. In fact, formal-methods tools and techniques are already of high quality and can address many non-trivial problems; we do give some technical recommendations on how tools and techniques can be made more accessible. To a greater extent, we focus on the human aspect: how to achieve impact, how to change the way of thinking of the various stakeholders about this issue, and in particular, as a research community, how to alter our behaviour, and instead of competing, collaborate to address this issue.