BBSYTER

Research programme

Work packages

1. Work package 01

   Generation of specifications, automatic property generation and feedback for non-expert users

   Led by Hugo De Sa Pereira Pinto Kaïs Klai

   A major obstacle to the adoption of formal verification is the need to express specifications in formal logics that non-experts often do not fully understand. WP1 assists non-experts in expressing their specifications and in understanding the results of the verification process in an easy manner.

   Expected outcomes

   • A reusable specification framework for automatically generating and refining formal models of smart-contract properties and vulnerabilities from friendly, comprehensive predefined templates, and for generating comprehensive feedback on the verification results.
   • A framework for the automatic generation and refinement of formal specifications of smart-contract properties from natural-language expressions and from smart-contract source code.
2. Work package 02

   Scalable verification of smart-contract ecosystems

   Led by Souheib Baarir Kaïs Klai

   Real-world smart contracts combine large persistent storage, an open environment with many potential callers and unbounded call sequences, and inter-contract calls whose nested invocations and reentrancy patterns induce enormous branching, so exhaustive exploration quickly becomes infeasible. WP2 structures scalability as a verification pipeline combining complementary reductions: property-directed reasoning and partial order reduction, symbolic exploration (BDDs and symmetries), and modularity and parallelism for multi-contract ecosystems.

   Expected outcome

   • Scalable verification methods enabling the analysis of large smart-contract ecosystems.
3. Work package 03

   Rewriting-logic-based symbolic verification

   Led by Souheib Baarir Carlos Olarte

   To integrate these techniques in a uniform way, WP3 relies on Rewriting Logic and its implementation in the Maude system: a flexible, intuitive and very expressive formalism that has proven very practical for many verification tasks (K framework, Real-Time Maude, Maude-NPA…). More powerful symbolic techniques in Maude open the way to more challenging verification tasks.

   Expected outcome

   • A rewriting-logic-based symbolic verification engine supporting SAT/SMT reasoning and scalable analysis.
4. Work package 04

   Dealing with inter-contract dependencies, concurrency and resource management

   Led by Munyque Mittelmann

   Smart-contract correctness depends not only on the contract itself but also on the users and contracts interacting with it, and vulnerabilities emerge when agents strategise to maximise their payoff. WP4 views a smart contract as a set of actions executed by multiple agents, with costs in tokens and gas, and defines correctness in strategic terms: a contract is correct from an agent's point of view if there exist strategies ensuring the desired outcomes regardless of the concurrent choices of other agents.

   Expected outcome

   • A strategy-logic modelling framework for interacting smart contracts, together with decision procedures for tractable fragments of the proposed logics.
5. Work package 05

   Integrating the scientific outputs into a unified software framework

   Led by Jaime Arias Hugo De Sa Pereira Pinto

   WP5 integrates the scientific outputs of the project into a unified, open-source framework: not just a research prototype, but a high-quality software asset with a robust architecture, exhaustive testing and well-written documentation, so that developers and researchers can reliably adopt, adapt and build upon our work.

   Expected outcome

   • A unified open-source verification environment that supports the specification of smart-contract vulnerabilities and custom temporal/strategic properties.

Open science

Open-source software

All the software developed in the project is open source and archived in Software Heritage.

Software Heritage

Open-access publications

All the publications of the project are deposited in HAL.

HAL