publications

2024

1. FAC

   Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL

   Diego Marmsoler, and Achim D. Brucker

   Formal Aspects Computing, Oct 2024

   Abs Bib HTML PDF

   Smart contracts are computer programs designed to automate legal agreements. They are usually developed in a high-level programming language, the most popular of which is Solidity. Every day, hundreds of thousands of new contracts are deployed managing millions of dollars’ worth of transactions. As for every computer program, smart contracts may contain bugs which can be exploited. However, since smart contracts are often used to automate financial transactions, such exploits may result in huge economic losses. In general, it is estimated that since 2019, more than $5B was stolen due to vulnerabilities in smart contracts. This paper addresses the issue of smart contract vulnerabilities by introducing an executable denotational semantics for Solidity within the Isabelle/HOL interactive theorem prover. This formal semantics serves as the basis for an interactive program verification environment for Solidity smart contracts. To evaluate our semantics, we integrate grammar-based fuzzing with symbolic execution to automatically test it against the Solidity reference implementation. The paper concludes by showcasing the formal verification of Solidity programs, exemplified through the verification of a basic Solidity token.

   @article{Marmsoler2024b,
     author = {Marmsoler, Diego and Brucker, Achim D.},
     title = {Isabelle/Solidity: A deep embedding of Solidity in Isabelle/HOL},
     year = {2024},
     publisher = {Association for Computing Machinery},
     address = {New York, NY, USA},
     issn = {0934-5043},
     url = {https://doi.org/10.1145/3700601},
     doi = {10.1145/3700601},
     journal = {Formal Aspects Computing},
     month = oct,
     keywords = {Solidity, Denotational Semantics, Isabelle/HOL},
   }

2. SEFM

   Secure Smart Contracts with Isabelle/Solidity

   Diego Marmsoler, Asad Ahmed, and Achim D. Brucker

   In Software Engineering and Formal Methods - 19th International Conference, SEFM 2024, Portugal, November 4-8, 2024, Proceedings, Oct 2024

   accepted, to be published

   Abs PDF

   Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. The framework consists of a novel formalization of the Solidity storage model, a shallow embedding of Solidity expressions and statements, an implementation of Isabelle commands to support a user in specifying Solidity smart contracts, and a verification condition generator to support a user in the verification. Compliance of the semantics is tested by a set of unit tests and the approach is evaluated by means of three case studies. Our results show that the framework can be used to verify even complex contracts with reasonable effort. Moreover, they show that the shallow embedding significantly reduces the verification effort compared to an alternative approach based on a deep embedding.

3. ICTAC

   Verifying Type Safety for Isabelle/Solidity

   Billy Thornton, and Diego Marmsoler

   In Theoretical Aspects of Computing - ICTAC 2024 - 21th International Colloquium, Bangkok, Thailand, November 25-29, 2024, Proceedings, Oct 2024

   accepted, to be published

   Abs PDF

   Smart contracts are programs stored on the blockchain that are often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions; thus, bugs can lead to large financial losses. In previous works, we developed a formalization of Solidity in Isabelle/HOL, which can be used to verify the properties of Solidity smart contracts. This formalization features untyped stores, where the types are inferred using type environment. It is currently unclear whether our semantics can cause type inconsistencies between stores and their environments. With this work we address this problem by formalizing the notion of type safety for untyped stores and verifying that our semantics preserve this property. The formalization and proofs were verified using Isabelle/HOL. Our results guarantee that our semantics are type safe and the proofs can be used to simplify the verification process for the properties of Solidity smart contracts.

4. FMTea

   Teaching Formal Methods in Application Domains - A Case Study in Computer and Network Security

   Achim D. Brucker, and Diego Marmsoler

   In Formal Methods Teaching - 6th Formal Methods Teaching Workshop, FMTea 2024, Milan, Italy, September 10, 2024, Proceedings, Oct 2024
5. FMBC

   Towards Mechanised Consensus in Isabelle

   Elliot Jones, and Diego Marmsoler

   In 5th International Workshop on Formal Methods for Blockchains (FMBC 2024), Oct 2024

   Abs Bib PDF

   A blockchain acts as a universal ledger for digital transactions between two parties that require no moderation from a third party. Such transactions are cheaper, quicker, and more secure with high traceability and transparency, with the decentralised structure of a blockchain network allowing for greater scalability and availability. For these reasons, blockchain is at the forefront of emerging technologies, with a wide variety of industries investing billions into the technology. A blockchains consensus protocol is what allows a blockchain network to be decentralised but can be subject to malicious behaviour and faults in its design and implementation that can lead to catastrophic effects like the DAO hack that resulted in a loss of $60 million. From this it is clear to see that the verifications of these protocols are paramount to ensure the safe use of blockchain. In this research, we formally verify the Proof-of-Work consensus protocol, used by Bitcoin, in Isabelle/HOL by modelling the blockchain as the longest branch in a binary tree and proving that the common prefix property holds with the assumption that the network is in majority honest. In this paper, we discuss the validity of our approach, key functions and lemmas we used to complete the proof, advantages and drawbacks of the model, related work and how this research can be taken further.

   @inproceedings{Elliot2024,
     author = {Jones, Elliot and Marmsoler, Diego},
     title = {{Towards Mechanised Consensus in Isabelle}},
     booktitle = {5th International Workshop on Formal Methods for Blockchains (FMBC 2024)},
     pages = {4:1--4:22},
     series = {Open Access Series in Informatics (OASIcs)},
     isbn = {978-3-95977-317-1},
     issn = {2190-6807},
     year = {2024},
     volume = {118},
     editor = {Bernardo, Bruno and Marmsoler, Diego},
     publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
     address = {Dagstuhl, Germany},
     url = {https://drops.dagstuhl.de/entities/document/10.4230/OASIcs.FMBC.2024.4},
     urn = {urn:nbn:de:0030-drops-198692},
     doi = {10.4230/OASIcs.FMBC.2024.4},
     annote = {Keywords: Formal Methods, Blockchain, Isabelle/HOL, Consensus, Verification, Theorem Provers},
   }

6. FACS(e)

   20th International Conference on Formal Aspects of Component Software (FACS 2024), Proceedings

   Diego Marmsoler, and Meng Sun

   Oct 2024
7. FMBC(e)

   5th International Workshop on Formal Methods for Blockchains (FMBC 2024), Proceedings

   Bruno Bernardo, and Diego Marmsoler

   Oct 2024

2023

1. SEFM

   SSCalc: A Calculus for Solidity Smart Contracts

   Diego Marmsoler, and Billy Thornton

   In Software Engineering and Formal Methods - 21st International Conference, SEFM 2023, Eindhoven, The Netherlands, November 6-10, 2023, Proceedings, Oct 2023

   Abs PDF

   Smart contracts are programs stored on the blockchain, often developed in a high-level programming language, the most popular of which is Solidity. Smart contracts are used to automate financial transactions and thus bugs can lead to large financial losses. With this paper, we address this problem by describing a verification environment for Solidity in Isabelle/HOL. To this end, we first describe a calculus to reason about Solidity smart contracts. The calculus is formalized in Isabelle/HOL and its soundness is mechanically verified. Then, we describe a Verification Condition Generator to automate the use of the calculus. Our approach can be used to verify the functional correctness of Solidity smart contracts. To demonstrate this, we use it to verify a simple token implemented in Solidity. Our results show that the framework has the potential to significantly reduce the verification effort compared to verifying directly from the semantics.

2022

1. AFP

   Isabelle/Solidity: A deep Embedding of Solidity in Isabelle/HOL

   Diego Marmsoler, and Achim D. Brucker

   Archive Formal Proofs, Oct 2022

   Abs HTML PDF

   Smart contracts are automatically executed programs, usually representing legal agreements such as financial transactions. Thus, bugs in smart contracts can lead to large financial losses. For example, an incorrectly initialized contract was the root cause of the Parity Wallet bug that saw $280M worth of Ether destroyed. Ether is the cryptocurrency of the Ethereum blockchain that uses Solidity for expressing smart contracts. We address this problem by formalizing an executable denotational semantics for Solidity in the interactive theorem prover Isabelle/HOL. This formal semantics builds the foundation of an interactive program verification environment for Solidity programs and allows for inspecting them by (symbolic) execution. We combine the latter with grammar based fuzzing to ensure that our formal semantics complies to the Solidity implementation on the Ethereum Blockchain. Finally, we demonstrate the formal verification of Solidity programs by two examples: constant folding and a simple verified token.

2. FAC

   Review on Modelling and Verification of Secure Exams: By Rosario Giustolisi Springer, Cham, 2018, X, 133 pp, ISBN: 9783319671062 (Hardback, GBP89.99), ISBN: 9783030097899 (Paperback, GBP64.99), ISBN: 9783319671079 (eBook, GBP51.99)

   Diego Marmsoler

   Formal Aspects Computing, Oct 2022
3. TAP

   Conformance Testing of Formal Semantics Using Grammar-Based Fuzzing

   Diego Marmsoler, and Achim D. Brucker

   In Tests and Proofs - 16th International Conference, TAP 2022, Held as Part of STAF 2022, Nantes, France, July 5, 2022, Proceedings, Oct 2022

   Abs PDF

   A common problem in verification is to ensure that the formal specification models the real-world system, i.e., the implementation, faithfully. Testing is a technique that can help to bridge the gap between a formal specification and its implementation. Fuzzing in general and grammar-based fuzzing in particular are successfully used for finding bugs in implementations. Traditional fuzzing applications rely on an implicit test specification that informally can be described as “the program under test does not crash”. In this paper, we present an approach using grammar-based fuzzing to ensure the conformance of a formal specification, namely the formal semantics of the Solidity Programming language, to a real-world implementation. For this, we derive an executable test-oracle from the formal semantics of Solidity in Isabelle/HOL. The derived test oracle is used during the fuzzing of the implementation to validate that the formal semantics and the implementation are in conformance.

2021

1. FMBC(e)

   3rd International Workshop on Formal Methods for Blockchains (FMBC 2021), Proceedings

   Bruno Bernardo, and Diego Marmsoler

   Oct 2021
2. Compositional Verification using Model Checking and Theorem Proving

   Diego Marmsoler

   In Model-Based Engineering of Collaborative Embedded Systems, Oct 2021
3. SEFM

   A Denotational Semantics of Solidity in Isabelle/HOL

   Diego Marmsoler, and Achim D. Brucker

   In Software Engineering and Formal Methods - 19th International Conference, SEFM 2021, Virtual Event, December 6-10, 2021, Proceedings, Oct 2021
4. Runtime verification for dynamic architectures

   Diego Marmsoler, and Ana Petrovska

   Journal of Logical and Algebraic Methods in Programming, Oct 2021

2020

1. Modeling and Verifying Dynamic Architectures with FACTum Studio

   Habtom Kahsay Gidey, Alexander Collins, and Diego Marmsoler

   In Formal Aspects of Component Software, Oct 2020

   Abs

   With the emergence of ambient and adaptive computing, dynamic architectures have become increasingly important. Dynamic architectures describe an evolving state space of systems over time. In such architectures, components can appear or disappear, and connections between them can change over time. Due to the evolving state space of such architectures, verification is challenging. To address this problem, we developed FACTum Studio, a tool that combines model checking and interactive theorem proving to support the verification of dynamic architectures. To this end, a dynamic architecture is first specified in terms of component types and architecture configurations. Next, each component type is verified against asserted contracts using nuXmv. Then, the composition of the contracts is verified using Isabelle/HOL. In this paper, we discuss the tool’s extended features with an example of an encrypted messaging system. It is developed with Eclipse and active on Github.

2. Formal methods in dependable systems engineering: a survey of professionals from Europe and North America

   Mario Gleirscher, and Diego Marmsoler

   Empir. Softw. Eng., Oct 2020
3. On the impact of architecture design decisions on the quality of blockchain-based applications

   Diego Marmsoler, and Leo Eichhorn

   Knowl. Eng. Rev., Oct 2020
4. FMBC(e)

   Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part I

   Emil Sekerinski, Nelma Moreira, José N. Oliveira, and 14 more authors

   Oct 2020
5. FMBC(e)

   Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II

   Emil Sekerinski, Nelma Moreira, José N. Oliveira, and 14 more authors

   Oct 2020
6. FMBC(e)

   2nd International Workshop on Formal Methods for Blockchains (FMBC 2024), Proceedings

   Bruno Bernardo, and Diego Marmsoler

   Oct 2020

2019

1. Towards Verified Blockchain Architectures: A Case Study on Interactive Architecture Verification

   Diego Marmsoler

   In Formal Techniques for Distributed Objects, Components, and Systems, Oct 2019

   Abs

   With the emergence of cryptocurrencies, Blockchain architectures have become more and more important. In such architectures, components maintain and exchange a list of records in a way which makes the entries persistent, i.e., resistant to modifications. Thereby, the architecture is dynamic in the sense that components may join or leave the network and connections between them may change over time. The dynamic nature of Blockchain architectures makes their verification a challenge, since it involves reasoning about potentially unbounded number of components. To this end, we developed FACTum, an approach for the specification and interactive verification of dynamic architectures based on the interactive theorem prover Isabelle. In this paper we report on the outcome of applying the approach to formally specify a version of Blockchain architectures and verify that the list entries of such architectures are indeed persistent.

2. JLAMP

   Detecting Architectural Erosion using Runtime Verification

   Diego Marmsoler, and Ana Petrovska

   In Proceedings 12th Interaction and Concurrency Experience, Copenhagen, Denmark, 20-21 June 2019, Oct 2019

   12th Interaction and Concurrency Experience
3. APML: An Architecture Proof Modeling Language

   Diego Marmsoler, and Genc Blakqori

   In Formal Methods – The Next 30 Years, Oct 2019

   Abs

   To address the increasing size and complexity of modern software systems, compositional verification separates the verification of single components from the verification of their composition. In architecture-based verification, the former is done using Model Checking, while the latter is done using interactive theorem proving (ITP). As of today, however, architects are usually not trained in using a full-fledged interactive theorem prover. Thus, to bridge the gap between ITP and the architecture domain, we developed APML: an architecture proof modeling language. APML allows one to sketch proofs about component composition at the level of architecture using notations similar to Message Sequence Charts. With this paper, we introduce APML: We describe the language, show its soundness and completeness for the verification of architecture contracts, and provide an algorithm to map an APML proof to a corresponding proof for the interactive theorem prover Isabelle. Moreover, we describe its implementation in terms of an Eclipse/EMF modeling application, demonstrate it by means of a running example, and evaluate it in terms of a larger case study. Although our results are promising, the case study also reveals some limitations, which lead to new directions for future work.

4. A denotational Semantics for Composition in Dynamic Architectures

   Diego Marmsoler

   In 2019 International Symposium on Theoretical Aspects of Software Engineering (TASE), Jul 2019

   Abs

   With the emergence of mobile and adaptive computing, dynamic architectures have become increasingly important. In such architectures, components can appear and disappear, and connections between them can change over time. Verification of such architectures is performed over the composition of its components, which is usually defined in an operational style. Sometimes however, a denotational style might be more convenient for verification. Thus, in the following paper, we propose a denotational semantics for composition in dynamic architectures based on fixed points in lattices. We show that it is well-defined by proving that fixed points are guaranteed to exist. Finally, we use our definition to derive a logical characterization of composition, which forms the basis of a framework for the interactive verification of dynamic architectures.

5. SCP

   A Calculus for Dynamic Architectures

   Diego Marmsoler

   Science of Computer Programming, Jul 2019

   Abs PDF

   With the emergence of mobile and adaptive computing, dynamic architectures have become increasingly important. In such architectures, components may appear or disappear, and connections between them may change over time. Dynamic architectures are usually specified in terms of two separate specifications: a specification of component behavior and a specification of component activation and reconfiguration. To verify them, both specifications are first interpreted over a common model for dynamic architectures and verified against a property specified over the same model. Interpreting the specifications over the model, however, introduce repetitive proof steps, which increase the length of proofs, and thus the effort to develop and maintain them. To address this problem, we developed a calculus for dynamic architectures providing rules to reason about component behavior in a dynamic environment. We proved soundness and relative completeness of the rules, implemented them in the interactive theorem prover Isabelle, and mechanized the corresponding soundness proofs. The calculus can be used to support the abstract verification of dynamic architectures in Isabelle. This is demonstrated by means of a running example and evaluated in terms of four case studies. Our results suggest that the calculus has the potential to reduce the length of proofs for the verification of dynamic architectures, thus reducing the effort to develop and maintain verification results.

6. FAC

   Interactive Verification of Architectural Design Patterns in FACTum

   Diego Marmsoler, and Habtom Kahsay Gidey

   Formal Aspects Computing, Jul 2019

   Abs PDF

   Architectural design patterns (ADPs) are architectural solutions to common architectural design problems. They are an important concept in software architectures used for the design and analysis of architectures. An ADP usually constrains the design of an architecture and, in turn, guarantees some desired properties for architectures implementing it. Sometimes, however, the constraints imposed by an ADP do not lead to the claimed guarantee. Thus, applying such patterns for the design of architectures might result in architectures which do not fulfill their intended requirements. To address this problem, we propose an approach for the verification of ADPs, based on interactive theorem proving. To this end, we introduce a model for dynamic architectures and a language for the specification of ADPs over this model. Moreover, we propose a framework for the interactive verification of such specifications based on Isabelle/HOL. In addition we describe an algorithm to map a specifi cation to a corresponding Isabelle/HOL theory over our framework. To evaluate the approach, we implement it in Eclipse/EMF and use it for the verification of four ADPs: variants of the Singleton, the Publisher-Subscriber, the Blackboard pattern, and a pattern for Blockchain architectures. With our approach we complement traditional approaches for the verification of architectures, which are usually based on automatic verification techniques such as model checking.

7. Axiomatic Specification and Verification of Architectural Design Patterns using Interactive Theorem Proving

   Diego Marmsoler

   Technische Universität München, Jul 2019
8. Verifying Dynamic Architectures using Model Checking and Interactive Theorem Proving

   Diego Marmsoler

   In Software Engineering and Software Management 2019, Jul 2019
9. Strategic logics for collaborative embedded systems

   Damian Kurpiewski, and Diego Marmsoler

   SICS Software-Intensive Cyber-Physical Systems, Jul 2019

   Abs

   In embedded systems, there is a clear movement from autonomous systems towards collaborative systems, forming so-called collaborative system groups (CSGs), which collaborate to achieve common goals. Verification of CSGs, however, imposes new challenges, which are difficult to address with traditional verification techniques. In the following, we investigate the use of strategic logics for the analysis of CSGs, by means of a use-case in the domain of smart production systems. Our results show that strategic model checking is useful to investigate certain aspects of CSGs, such as the impact of environmental changes. However, our results also show some limitations of the approach, when it comes to the analysis of implementation-level aspects, such as performance. Thus, we conclude that strategic model checking might complement existing approaches for the analysis of CSGs.

2018

1. A Framework for Interactive Verification of Architectural Design Patterns in Isabelle/HOL

   Diego Marmsoler

   In The 20th International Conference on Formal Engineering Methods, ICFEM 2018, Proceedings, Jul 2018
2. On Syntactic and Semantic Dependencies in Service-Oriented Architectures

   Diego Marmsoler

   In 12th International Symposium on Theoretical Aspects of Software Engineering, Jul 2018
3. Hierarchical Specification and Verification of Architecture Design Patterns

   Diego Marmsoler

   In Fundamental Approaches to Software Engineering - 21th International Conference, FASE 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings, Jul 2018

   PDF
4. A Theory of Architectural Design Patterns

   Diego Marmsoler

   Archive of Formal Proofs, Mar 2018

   \urlhttp://isa-afp.org/entries/Architectural_Design_Patterns.html, Formal proof development
5. FACTUM Studio: A Tool for the Axiomatic Specification and Verification of Architectural Design Patterns

   Diego Marmsoler, and Habtom Kahsay Gidey

   In Formal Aspects of Component Software - FACS 2018 - 15th International Conference, Proceedings, Mar 2018
6. Simulation-Based Analysis of Blockchain Architectures

   Diego Marmsoler, and Leo Eichhorn

   In The 3rd Symposium on Distributed Ledger Technology, SDLT 3, Proceedings, Mar 2018

2017

1. Towards a Calculus for Dynamic Architectures

   Diego Marmsoler

   In Theoretical Aspects of Computing - ICTAC 2017 - 14th International Colloquium, Hanoi, Vietnam, October 23-27, 2017, Proceedings, Mar 2017
2. Verifying Patterns of Dynamic Architectures using Model Checking

   Diego Marmsoler, and Silvio Degenhardt

   In Proceedings International Workshop on Formal Engineering approaches to Software Components and Architectures, FESCA@ETAPS 2017, Uppsala, Sweden, 22nd April 2017., Mar 2017
3. Dynamic Architectures

   Diego Marmsoler

   Archive of Formal Proofs, Jul 2017

   HTML
4. Grounded Architectures: Using Grounded Theory for the Design of Software Architectures

   Habtom Kahsay Gidey, Diego Marmsoler, and Jonas Eckhardt

   In 2017 IEEE International Conference on Software Architecture Workshops (ICSAW), Apr 2017
5. Research Challenges for a Future-Proof E/E Architecture - A Project Statement

   Stefan Kugele, Vadim Cebotari, Mario Gleirscher, and 8 more authors

   In INFORMATIK 2017, Apr 2017
6. On the Semantics of Temporal Specifications of Component-Behavior for Dynamic Architectures

   Diego Marmsoler

   In Eleventh International Symposium on Theoretical Aspects of Software Engineering, Apr 2017

2016

1. On Activation, Connection, and Behavior in Dynamic Architectures

   Diego Marmsoler, and Mario Gleirscher

   Scientific Annals of Computer Science, Apr 2016
2. ICTAC

   Specifying Properties of Dynamic Architectures using Configuration Traces

   Diego Marmsoler, and Mario Gleirscher

   In International Colloquium on Theoretical Aspects of Computing, Apr 2016

   Abs PDF

   The architecture of a system describes the system’s overall organization into components and connections between those components. With the emergence of mobile computing, dynamic architectures became increasingly important. In such architectures, components may appear or disappear, and connections may change over time. Despite the growing importance of dynamic architectures, the specification of properties for those architectures remains a challenge. To address this problem, we introduce the notion of configuration traces to model properties of dynamic architectures. Then, we investigate these properties to identify different types thereof. We show completeness and consistency of these types, i.e., we show that (almost) every property can be separated into these types and that a property of one type does not impact properties of other types. Configuration traces can be used to specify general properties of dynamic architectures and the separation into different types provides a systematic way for their specification. To evaluate our approach we apply it to the specification and verification of the Blackboard pattern in Isabelle/HOL.

3. Verification of component architectures using mode-based contracts

   S. Kugele, Diego Marmsoler, N. Mata, and 1 more author

   In 2016 ACM/IEEE International Conference on Formal Methods and Models for System Design (MEMOCODE), Nov 2016

2015

1. A Model of Layered Architectures

   Diego Marmsoler, Alexander Malkis, and Jonas Eckhardt

   In Proceedings 12th International Workshop on Formal Engineering approaches to Software Components and Architectures, FESCA 2015, London, United Kingdom, April 12th, 2015., Nov 2015
2. A Model of Service-Oriented Architectures

   Alexander Malkis, and Diego Marmsoler

   In Components, Architectures and Reuse Software (SBCARS), 2015 IX Brazilian Symposium on, Nov 2015

2014

1. Towards a Theory of Architectural Styles

   Diego Marmsoler

   In Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering - FSE 2014, Nov 2014

2013

1. On the laws of failure: a theory of compensable programs

   Diego Marmsoler

   In Eurocon 2013, Jul 2013
2. On the Laws of Failure: A Theory of Compensable Programs

   Diego Marmsoler

   Universität Augsburg, Lunwig Maximilan Universität München, Technische Universität München, Jul 2013

2010

1. Applying the Scientific Method in the Definition and Analysis of a new Architectural Style

   Diego Marmsoler

   Free University of Bolzano, Jul 2010