Online Discussion

September 29, 2021, 12:00 UTC - 14:00 UHR UTC
September 29, 2021, 14:00 CEST -16:00 UHR CEST
September 29, 2021, 08:00 EDT - 10:00 UHR EDT

Information for participating are below.

The VerifyThis Collaborative Large Scale Challenge aims at proving that deductive program verification can produce relevant results for real systems with acceptable effort. We selected HAGRID, a recently developed PGP-keyserver, for the challenge. Its development became necessary as the old keyserver had serious data protection and security issues.

Agenda: We will continue and deepen this discussion by means of a concrete example to be specified in this meeting. By discussing how automata-related and contract-related specification artifacts could be formulated, we plan to identify particular benefits from the viewpoints. Moreover, it will allow us to constructively think about ideas how such specifications can be integrated.

In April 2020 four approaches to the verification challenge have been submitted to and presented during an online workshop, and in November 2020, a follow-up online discussion revealed interesting new ideas regarding specification and verifiation of interacting systems like Hagrid.

We will continue and deepen this discussion by means of a concrete example to be specified in this meeting. By discussing how automata-related and contract-related specification artifacts could be formulated, we plan to identify particular benefits from the viewpoints. Moreover, it will allow us to constructive think about ideas how such specifications can be integrated.

Aggregated Materials

Who can join the meeting?

Everybody who is interested in the challenge, formal verification, the proposed solutions or VerifyThis is cordially invited to join the meeting!

How can I join the meeting? {#participating}

The online event takes place with Zoom.

In protection against spammers, we require a short registration beforehand. The login credentials will be sent via your provided email address. Please register yourself with an email to weigl@kit.edu.

Note: If you had already registered for the Online Event in November or Feburary, or June we will send you the required login credentials automatically. Another registration is not required in this case.

Discussion summary

September 29, 2021

During the last discussion, the feedback was that participants would like to discuss concrete examples. Therefore, Wolfgang Ahrendt prepared a concrete example for this discussion.

The example will be introduced, then we will split into different breakout rooms (where the discussion is not summarised) and at the end of the meeting, we put everything together.

The example models a Casino Game (and is due to Gordon Pace), encoded as a Solidity smart contract.

There is 1 operator, and at most 1 player (opponent).

The state space of the game consists of:

Initially both, pot and bet, are empty (i.e. 0). The hashed secret and the guess have a default value. The program allows the following operations:

The idea would be that the code ensures that the player can get the money by calling decide bet. In smart contracts: calling a method and money transfer are done hand-in-hand.

In this example, all the money is modeled in the game. Variants are possible, where the operator can enforce the player to pay a fee to place a bet.

The code has several challenges. It would be possible to create a denial of service contract that enters the casino as a player. The transfer method of that malicious contract might be implemented wrongly, by refusing payment (require(false); on the transfer method). In that case, the state would always roll back, and the game state would never become idle anymore. The player might not be able to win anything, but it does damage to the operator who can no longer claim back money in the pot.

There are solutions, like using the send method, that allows to check if the payment actually succeeded.

In parallel there was a discussion about how to express absence of denial of service attacks, by using temporal properties like AG EF (state = idle).

We then split into three break out rooms:

After the breakout rooms, the groups reported back.

  1. Temporal Properties

    The temporal properties group started drawing automata-like specifications. However, interesting points such as roll back are not discussed yet. These specifications would then enable one to verify liveness properties such as the AG EF (state = idle).

    To precisely capture the temporal properties, it would be important to know about the language semantics.

    Gidon asked if the triangle operator (discussed in an earlier meeting) could be useful here.

    Another discussion point was the level of granularity for such specifications. In many approaches we expect contracts for any method call. This led to the discussion in the contract specification group.

  2. Contract Specifications

    This group started to add pre- and postconditions, assuming a special built-in specification variable \balance, to describe the behaviour of payable methods. The group suggested to add an invariant to specify the relation between the blockchain's balance and the variables (pot and bet, in this case)

    Their conclusion was that we need some kind of revert preconditions, which indicate under which conditions a rollback could happen. Ideally this would be transitive, thus in the decideBet method, we would specify that the state could also roll back if the revert precondition of the transfer method (call within decideBet method) would hold. You don't need to specify the effect of the roll back explicitly - it's just resetting everything, and all changes are lost.

    Wolfgang explained that in smart contracts, you often have no access to the external code, so you have to be defensive about what it could do. Specifiers and programmers have to be aware of this, and thus for example for the decideBet method, you would always assume that the transfer method that is called, could lead to a roll back.

    Gidon was wondering if you could also specify that you would revert if you don't have enough money in the blockchain. But the invariant guarantees in this particular example that this can never be the case.

  3. Security

    The security group discussed that security is by definition important, because smart contracts are about money, and they are open systems.

    The group then discussed about potential relevant properties, such as non-interference (making sure that private does not become public) and if relational properties could be of use. You can compare different runs of the systems. If one run would be able to get blocked, this would potentially be a loss of money.

    More thinking would be needed about what are relevant security properties.

    Wolfgang adds that for many people all properties such as no money is lost are security relevant, as this guarantees data integrity.

    Wolfgang then discussed a fix that would avoid the problem of the game never getting to the idle state. Rather than sending money around directly, the system would separate the game and the sending of the money. If a player wins, money is earmarked for the transfer. The transfer is then done by a special withdraw method, which will start the transfer. However, again care is needed here, the money needs to be bookmarked as 'withdrawn' before the actual transfer takes place, otherwise a malicious player could do a call back on withdraw, and receive the money multiple times.

During the next meeting, we will continue the discussion on this example and we will focus on the interaction between the temporal and the contract specifications. In the mean time, all groups are invited to think more about how to specify the behaviour of the program.