---
title: "Obligation Mechanism in Gobra"
author: [Hugo Queinnec]
date: "25.04.2023"
lang: "en"
...

# Obligation Mechanism in Gobra
Hugo Queinnec — Supervised by Linard Arquint

## Motivation

The goal of my master's thesis is to design a methodology to ensure the secure deletion of outdated sensitive data in protocol implementations. This would allow proving high-level security properties for protocol implementations, like forward secrecy. We aim for a language-agnostic methodology, but we will focus mainly on Go implementations and the Gobra verifier.

In order to prove that a value will be deleted at some point, we first have to characterize *timing* in the protocol. This is done by defining a *version number* $i$ that indicates temporality. Initially, the protocol has version $0$, and then the version number is incremented at some times to represent new protocol phases. Such increments are performed by calling a method `bumpVersion(currentVersion int)` that shifts the protocol version number from $i$ to $i+1$.

Then, we want to ensure that when bumping the protocol version to $i+1$, all existing (heap) values are meant to exist in this version. Previous values that are no longer useful must have been deleted. Typically, this happens in a protocol that continuously derives new keys from old ones: in this case when bumping the version, the newly generated key should be kept, while the old key should be deleted.

To do so, we use a mechanism of *obligations*. Upon creation of a time-sensitive value, an obligation is systematically created, linking the value to a *version* number $i$. Then, when bumping the protocol version, we check all existing obligations and ensure that they are valid: in our case that, we check the obligation version is equal to the new version number. Old obligations must be *discharged* before bumping, by using a method `deleteSafely` that safely deletes the value from memory, and is the only way to discharge the obligation.

This is why we want to add a general obligation mechanism to Gobra. It would be composed of two main parts: an obligation declaration, and a way of checking the presence of obligations (i.e., a leak check). In the following, we use the Gobra obligation `MemV(k []byte, v int)`, for a slice of bytes `k` with version `v`. The obligation is created upon creation of the time-sensitive bytes. It is similar to an abstract predicate, and represents both the permission to access the bytes in memory, and the obligation to delete them from memory before the protocol version bumps.

## Leak checks

### Idea

In order to have a way of checking all existing obligations, we have to ensure that all obligations are present in the frame in which we evaluate the leak check. Indeed, in the Viper example below, the method `bumpVersion` cannot check the obligation `MemV(k, i)` because it does not appear in its scope.

method main(key: Ref, version: Int)
    requires MemV(key, i) // MemV obligation in scope
{
    call(key, i)
}

method call(key: Ref, version: Int)
{
    bumpVersion(i) // Does not see any MemV obligation
}

To solve this problem, we also use *leak checks* to ensure that all obligations are passed to the called method. We define it the following way (in Viper):

define leak_check ([true, forperm k: Ref, v: Int [MemV(k, v)] :: false])

The idea is to add this `leak_check` as an additional precondition and postcondition to all methods in the Viper AST generated by Gobra.
When adding `leak_check` as a pre and postcondition to all methods, we ensure that all obligations are passed to the called method and then returned at the end of the method. This way, all obligations will be in the frame in which `bumpVersion` is called and thus we can check properties about these obligations.

However, one problem remains: it would be a lot of verification work to pass all obligations to all methods, especially considering that only methods that contain a `bumpVersion`[^1] call need to have these obligations. Let's consider the following example to illustrate a possible solution:

[^1]: By "contain a `bumpVersion` call", we mean methods that call `bumpVersion` directly or indirectly (i.e. methods that call a method that calls `bumpVersion`, and so on recursively).

method main(key: Ref, version: Int)
    requires MemV(key, i)
    requires leak_check
    ensures leak_check
{
    call_bump(key, i)
    call_no_bump()
}

method call_bump(key: Ref, version: Int)
    requires MemV(key, i)
    requires leak_check
    ensures MemV(key, i)
    ensures leak_check
{
    bumpVersion(i) // all obligations are in the current frame
}

method call_no_bump() // Will not call `bumpVersion`
    ensures leak_check
{
    // ...
}

Here, `main` and `call_bump` (directly or indirectly) contain a call to `bumpVersion`, and thus need to pass all obligations, requiring `leak_check` as a precondition and a postcondition. However, *if we know* that `call_no_bump` will not call `bumpVersion`, we can remove the `leak_check` precondition because we do not have to check properties about all obligations in its frame, i.e., we can permit that obligations are framed around the `call_no_bump()` call. However, the postcondition `leak_check` is necessary, to enforce that all obligations are returned at the end of the method.

This methodology significantly reduces annotation overhead assuming there will be very few calls to `bumpVersion` in the protocol implementation. One major point remains: how do we know if a method contains a call to `bumpVersion` or not? We explain below two approaches to solve this problem.

### First approach: fractional permissions

We use an abstract predicate `can_bump()` to which full permissions are necessary to call `bumpVersion`. This resource is a free precondition of the `main` method. Intuitively, we allow framing of obligations when a fraction of `can_bump()` remains in the current frame.
<!--
In pseudocode, the leak check performed as a precondition will look as follows:

requires ({callee is given full bump_perm() permission} ==> leak_check)

The part in curly brackets is something that looks like a `perm` expression in Viper, but it is a bit more complicated. First, perm expressions can only be used in a Viper *inhale-exhale* expression. Using `perm` in the *exhale* part means that we can check the permission amount of `bump_perm()` owned by the *caller* and not the *callee*.
\newpage

We could then check if the caller has a full permission to `bump_perm()` *before* eventually giving it to the callee, but it wouldn't work[^2]. Instead, we check if the caller has no permission to `bump_perm()` *after* passing all permissions to the callee. This would not ensure that the callee has the full permission to `bump_perm()`, but if the caller keeps a fraction of `bump_perm()` permission, it would ensure that the callee cannot call `bumpVersion`, making the methodology sound[^3].

[^2]: We could have the case where the programmer would encapsulate the `bump_perm()` permission into another predicate. Therefore, the *caller* would seemingly not have full permission to `bump_perm()` (without *unfolding* the encapsulating predicate), and no precondition leak check would be done, even though the full `bump_perm()` permission could be passed to the caller.

[^3]: And if the programmer forgets to give a `bump_perm()` permission fraction to a callee, it is not an issue for soundness, but it will have two consequences. First, the callee (and following subcalls) won't be able to call `bumpVersion`. Second, the methods called by the callee that has received no `bump_perm()` permission will necessarily have an entry leak check, which will increase the verification effort.
-->
Therefore, we add the following precondition leak check to all methods, as their *last* precondition:

define check_caller ([true, perm(can_bump()) == none ==> leak_check])

To reduce verification effort, it will be in the interest of the programmer to keep a fraction of `can_bump()` in the caller's frame whenever possible. This can be done by always passing half of the current permission amount to the callee. The callee should always return the provided `can_bump()` fraction, otherwise it would be impossible to call `bumpVersion` later on.

Ultimately, the Viper code of the previous example would look as follows:

method main(key: Ref, version: Int)
    requires can_bump() // Full permission initially given to main
    requires MemV(key, i)
    requires check_caller // Auto generated
    ensures leak_check // Auto generated
{
    call_bump(key, i)
    call_no_bump()
}

method call_bump(key: Ref, version: Int)
    requires can_bump()
    requires MemV(key, i)
    requires check_caller // Auto generated -> enforces that `MemV(key, i)` is given
    ensures can_bump()
    ensures MemV(key, i)
    ensures leak_check // Auto generated -> enforces that `MemV(key, i)` is returned
{
    bumpVersion(i) // all obligations are in the current frame
}

method call_no_bump() // Will not call `bumpVersion`
    requires acc(can_bump(), 1/2)
    requires check_caller // Auto generated -> NOP because caller still has partial permission to can_bump()
    ensures acc(can_bump(), 1/2)
    ensures leak_check // Auto generated
{
    // ...
}

Leak checks are automatically generated for all methods. The programmer only has to handle `can_bump()` in pre and postconditions of all methods (2 lines per method), which should be less work than always passing all obligations (2$n$ lines per method for $n$ obligations).

### Second approach: non-hideable structure

The first solution is acceptable, but still requires the programmer to handle `can_bump2()`[^3] in pre- and postconditions of all methods. This second approach aims to reduce the programmer's work even further, but will require some new Gobra structures.

[^3]: We use `can_bump2()` to better distinguish the two approaches while the intuition behind `can_bump2()` remains the same, i.e., full permissions allow a call to `bumpVersion`.

In a nutshell, the idea is to allow framing of obligations unless full permissions to `can_bump2()` are specified in a callee's precondition.
However, we have to ensure that `can_bump2()` cannot be "hidden" in another predicate and/or lock or channel invariant, which would otherwise render this approach unsound.

This is why for this solution, we have to introduce a new annotation to define the `can_bump2` predicate as "non-hideable". "non-hideable" intuitively expresses that this predicate can only occur in pre- and postconditions and, in particular, cannot be mentioned in bodies of other predicates.

With this approach, the programmer only has to specify full `can_bump2()` permissions in method preconditions that (directly or indirectly) contain a `bumpVersion` call (a lot less work than the first approach, assuming the protocol only contains a few bump calls). The Viper code of the previous example would thus look as follows:

method main(key: Ref, version: Int)
    requires can_bump2() // Non-hideable predicate, full permission initially given to main
    requires MemV(key, i)
    requires leak_check // Auto generated because of `can_bump2()`
    ensures leak_check // Auto generated (always)
{
    call_bump(key, i)
    call_no_bump()
}

method call_bump(key: Ref, version: Int)
    requires can_bump2()
    requires MemV(key, i)
    requires leak_check // Auto generated because of `can_bump2()`
    ensures MemV(key, i)
    ensures leak_check // Auto generated (always)
{
    bumpVersion(i) // all obligations are in the current frame
}

method call_no_bump() // Will not call `bumpVersion`
    ensures leak_check // Auto generated (always)
{
    // ...
}

## Syntax

We now present Gobra syntax for the two approaches mentioned above.

### First approach: obligation check defined in Gobra

This first approach puts most control in the hands of the programmer, and requires only minimal additions to the Gobra syntax.

// General syntax
obligation [Assertion A] OblExample(...) // A is a pure expression

// Our case of memory deletion
obligation [perm(can_bump()) == none] MemV(k ByteString, v int)

The assertion `A` written between square brackets[^4] is used to specify when to perform the precondition leak check (in the first leak check approach). With the second leak check approach, we would not need an assertion anymore, one should just specify the name of the non-hideable predicate that will be used to generate the precondition leak check, here `can_bump()`.

[^4]: `A` is not written in the obligation body to not give the *false intuition* that it could be folded like a predicate.

With this approach, we define the `bumpVersion` method **in Gobra** as follows, where `cur_version_byte_slices` allows a programmer to specify all slices of bytes that will be passed from the previous to the current version (these have to have the right version number as specified in the precondition):

type ByteString []byte
type ValueSet set[ByteString]

requires can_bump()
requires forall s ByteString :: s in cur_version_byte_slices ==> MemV(s, oldVersion+1)
// Viper: `requires check_caller` (generated by Gobra)
ensures can_bump()
ensures forall s ByteString :: s in cur_version_byte_slices ==> MemV(s, oldVersion+1)
// Viper: `ensures leak_check` (generated by Gobra)
func bumpVersion(oldVersion int, cur_version_byte_slices ValueSet)

Leak checks will ensure that all existing `MemV` obligations are in the frame when calling `bumpVersion`. We then pass all `MemV` obligations to `bumpVersion`, by specifying them as the parameter `cur_version_byte_slices` (this is the responsibility of the programmer).

Because `bumpVersion` is a method that receives full `can_bump()` permission, there will be an entry leak check generated by Gobra, which will prevent the programmer from forgetting any `MemV` obligation in `cur_version_byte_slices`. Additionally, as the precondition `requires forall s ByteString :: s in cur_version_byte_slices ==> MemV(s, oldVersion+1)` relates the `MemV` version to the `bumpVersion` version, it enforces that the programmer will only be able to specify `MemV` obligations with the correct version in `cur_version_byte_slices`. Therefore, `MemV` obligations with past versions will have to be safely deleted before calling `bumpVersion`. Otherwise, verification fails, as intended.

Additionally, the implementation of this approach together with the first leak check approach relies for our case on the existence of the `perm` keyword in Gobra. As it does not exist yet, we will need to implement it with the same semantics as in Viper.

<!-- Also, giving all `MemV` permissions to `bumpVersion` may require adding some additional postconditions to `bumpVersion`. Indeed, if the caller needs to ensure an expression given by a pure function that requires `MemV`, then `bumpVersion` should show that the value of the function has not changed. This is additional verification work for the programmer. -->

### Second approach: obligation check generated in Viper

This second approach is a suggestion with a syntax that is more restrictive but that reduces the annotation overhead.

// General syntax
obligation OblExample(...) [method OblCheck(...) :: pred OblCheckPred()] {
    Assertion B
}

// Our case of memory deletion
obligation MemV(k ByteString, v int) [method bumpVersion(oldVersion int) :: pred can_bump2()] {
    v == oldVersion + 1
}

This syntax relates the obligation (`MemV`), the obligation check method (`bumpVersion`) and its non-hideable predicate `can_bump2()`. The assertion `B` is not the same as before: it is the assertion that `bumpVersion` will check on all obligations (the assertion uses parameters of both `bumpVersion` and `MemV`). This syntax does not give control on the precondition leak check condition[^5]. This allows to remove the responsibility of the programmer to define `bumpVersion`: it can be fully generated **in Viper**:

[^5]: The precondition leak check would be generated with either the first or second leak check approach, depending only on `can_bump()` and `can_bump2()`, respectively.

method bumpVersion(oldVersion: Int)
    requires[true, forperm k: Ref, v: Int [MemV(k, v)] :: v == oldVersion + 1]
    requires can_bump2()
    ensures can_bump2()

Contrarily to the first approach, the programmer does not have to pass all `MemV` permissions to `bumpVersion`. Instead, `bumpVersion` will check the condition on all `MemV` obligations in the current frame (which are all existing `MemV` thanks to the leak checks). `bumpVersion` method is here *special-cased* to not have entry and exit leak checks.

With this approach, there is no need to introduce `perm` or `forperm` in Gobra, as they are only occur in the generated Viper code.

However, this approach requires adding a lot of specific syntax to Gobra, which may be challenging to parse. Additionally, the added syntax will be useful only for very specific use cases (in particular, it restricts the entry leak check condition to being related to the ownership of some abstract predicate or non-hideable structure).

Also, this syntax is too specific for the case where we would have several *obligation check* methods (for the same type of obligation), each with its own condition. Indeed, we would need to provide a list of obligation check methods, a list of obligation check predicates, and a list of obligation check conditions (the latter being impossible with this syntax where the condition is the obligation body).

## Conclusion

In order to introduce an obligation mechanism to Gobra, we have presented two approaches to handle leak checks, and two approaches to define the Gobra syntax. Each approach has its pros and cons, which should be taken into account in order to make a decision on the implementation.