Verification with Prusti

[zgrannan]

For the past few months I've been looking at using Prusti to verify the correctness of ibc-rs, in particular the modules and relayer crates. The purpose of this PR is just to share a bit of what I've been able to accomplish so far and explain what an integration would look like. Also please let me know if you have any feedback or questions. This PR is not intended to be merged.

The Prusti verification operates on entire crates, and is done via an external tool. Prusti verification does not require introducing any new dependencies on the project. Specifications can be encoded as attributes that are only enabled when the "prusti" flag is set, i.e. #[cfg_attr(feature="prusti", <spec>)]. The specification syntax is a superset of Rust, with extensions to support forall expressions etc.

However, Prusti does not currently support all Rust language features and datatypes. So, it is also possible to provide different implementations for Prusti verification only (i.e. to work-around unsupported language features), without changing the actual implementation.

The following describes what I've done so far. A large caveat is that verification required changes to the code to remove unsupported features and datatypes; and some parts of the code containing unsupported features were excluded from verification entirely. The code in this PR only includes the added specifications, without the changes, in order to clearly demonstrate the annotation syntax and invariants. As a result, Prusti won't be able to verify the code in this PR; a version that has removed unsupported features is available here. Note that it is still a bit messy.

Verification of Safety Properties

Prusti was able to verify safety properties on the modules and relayer crate, with the caveat the properties may not hold for code unsupported by Prusti.

No function will trigger panic!

For example in context.rs:

#[cfg_attr(feature="prusti", requires(self.max_history_size > 0))]
#[cfg_attr(feature="prusti", requires(target_height.revision_height <= u64::MAX))]
#[cfg_attr(feature="prusti", requires(target_height.revision_number == self.latest_height.revision_number))]
#[cfg_attr(feature="prusti", requires(target_height.revision_height >= self.latest_height.revision_height))]
pub fn with_height(self, target_height: Height) -> Self {
    if target_height.revision_number > self.latest_height.revision_number {
        unimplemented!()
    } else if target_height.revision_number < self.latest_height.revision_number {
        panic!("Cannot rewind history of the chain to a smaller revision number!")
    } else if target_height.revision_height < self.latest_height.revision_height {
        panic!("Cannot rewind history of the chain to a smaller revision height!")
    } else if target_height.revision_height > self.latest_height.revision_height {
        // Repeatedly advance the host chain height till we hit the desired height
        let mut ctx = MockContext { ..self };
        while ctx.latest_height.revision_height < target_height.revision_height {
            ctx.advance_host_chain_height()
        }
        ctx
    } else {
        // Both the revision number and height match
        self
    }
}

The annotations ensure that the function with_height() will not panic, and introduces an obligation on the caller to ensure preconditions are satisfied.

Calls to Option.unwrap and Result.unwrap will not panic

For example, for serialization:

#[cfg_attr(feature="prusti", requires(Hex::upper_case().encode_to_string(data).is_ok()))]
pub fn ser_hex_upper<S, T>(data: T, serializer: S) -> Result<S::Ok, S::Error>
where
    S: Serializer,
    T: AsRef<[u8]>,
{
    let hex = Hex::upper_case().encode_to_string(data).unwrap();
    hex.serialize(serializer)
}

Arithmetic Operations will not overflow

This is useful, for example, operations on Height, to ensure that it is monotonically increasing.

#[cfg_attr(feature="prusti", requires(u64::MAX - self.revision_height >= delta))]
pub fn add(&self, delta: u64) -> Height {
    Height {
        revision_number: self.revision_number,
        revision_height: self.revision_height + delta,
    }
}

#[cfg_attr(feature="prusti", requires(self.revision_height < u64::MAX))]
pub fn increment(&self) -> Height {
    self.add(1)
}

Functional Correctness

It was also possible to prove domain-specific invariants and correctness properties.

Misbehavior Detection

In tendermint.rs we have proven that:

• In the event of misbehaviour, the timestamp for the witness header is after the timestamp of all of the supporting headers

The invariant is specified as:

predicate! {
    fn misbehaviour_invariant(m: &MisbehaviourEvidence) -> bool {
    forall(
        |i : usize|
        (0 <= i && i < m.supporting_headers.len() ==>
          get_supporting_header_time(&m.supporting_headers, i) < get_witness_time(&m.misbehaviour)))
    }
}

• The witness header is within the trust period

This invariant asserts header_within_trust_period from the Tendermint crate.

Proving these invariants require adding and proving additional invariants of other functions.

Client Keeper

In ibc.rs, we prove that store_client_result in ClientKeeper, will correctly maintain an invariant about the stored client data. This is done out of the codebase, because the separation of ClientKeeper and ClientReader traits.

The client invariant corresponds to:

fn client_invariant(client: &MockClientRecord) {
    match client.client_state {
        Some(cs) =>
            match client.consensus_states.keys().max() {
                Some(max_height) => cs.latest_height() == max_height,
                None => false
            },
        None => client.consensus_states.is_empty()
    }
}

[adizere]

Hi @zgrannan. Thank you for your work here!

Am I correct in understanding that this PR is a proof of concept wrt. Prusti-based testing integration in ibc-rs? Let us know if there are specific topics you'd like us to weigh in or provide feedback. Note that we'll go ahead and close this PR unless there is anything specific we can follow-up with.

In particular the panic and arithmetic overflow guards would be very interesting for us, since we had prior experience where this kind of problems can occur and are not always easy to catch (ref #1885 #1555 #1442 #1122).