Move "MAC assumption" deeper

[henriman]

At the moment, we simply assume that hf_valid holds after the comparison in router/dataplane.go, verifyCurrentMAC. This PR moves the assumption deeper into the code (into path.FullMAC), by instead assuming that the abstraction of the result of path.FullMAC equals the abstract computation of the MAC on the abstraction of the info and hop fields.

Besides slightly reducing the assumption, this change is necessary in order to be able to declassify the MAC tag when proving secure information flow (cf. #394, #409): This needs to happen before comparing it to the given tag (using subtle.ConstantTimeCompare in verifyCurrentMAC, processOHP) -- to satisfy low control flow, but also because the result of this comparison is exactly what is leaked about the router's key. Consequently, we need to abstractly describe that FullMAC/MAC compute such MAC tags s.t. we can allow declassification at this point.

---

Approach

In order to keep track of which AS's secret key is used by the hash instances produced by DataPlane.macFactory/by the hash instance saved in scionPacketProcessor.mac, we define an extension of the hash.Hash interface called ScionHashSpec which allows us to access the corresponding AS identifier using function ScionHashSpec.Asid.

• We decided to extend the interface instead of adding Asid directly to hash.Hash as this is specific to VerifiedSCION. Consequently (as e.g. scionPacketProcessor.mac needs to remain of type hash.Hash), we save the ScionHashSpec "version" of mac in scionPacketProcessor.macSpec and relate them using mac === macSpec.
• We establish that Asid returns the correct AS identifier in SetKey (using the appropriately adapted InitMac function). This information is then propagated for p scionPacketProcessor using p.macSpec.Asid() == dp.Asid().

In FullMAC/MAC, besides h hash.Hash we then also pass sh hash.ScionHashSpec (where h === sh); this allows us to describe the corresponding abstract computation by passing sh.Asid() to io.nextMsgtermSpec.

See the comments below for further discussion explaining the need for this approach.

---

Status

This is done. However, as I needed to adapt the contracts of SetIA and ´SetKey, one _should_ adapt router/dataplane_spec_test.gobra` to show that these contracts are satisfiable (although I am certain they are).

Adapting router/dataplane_spec_test.gobra.

As the current tests don't call SetIA or SetKey, but rather set these fields directly, this requires a few modifications. The main issue that I came across was the fact that we pass full permissions to (*DataPlane).Mem (counting the permissions in the mutex) to these methods; consequently, after a call to e.g. SetIA, we are not able to establish that some properties dependent on unrelated fields of DataPlane still hold.

I have started adapting this test in branch mac-assumption-dataplane-test of my fork of VerifiedSCION (though I did not come far). The approach I have taken thus far was to change the contracts of SetIA, SetKey to only require partial permissions to (*DataPlane).Mem and full permissions to the fields that are actually modified.

However, this is not very clean. @jcp19 suggested the following approach instead:

• Introduce a spec/abstract version of DataPlane which contains only the relevant fields, without permissions (e.g. save a seq instead of a slice).
• Introduce a function Abs that returns such an abstraction for a given DataPlane.
• Then for each method that we want to annotate in this way, introduce a function that performs the corresponding modification on the abstraction. E.g. for SetIA, we could have the following function:

ghost type DataPlaneSpec ghost struct {
    ...
    localIA addr.IA
    ...
}

ghost
pure func (d DataPlaneSpec) UpdateIA(ia addr.IA) DataPlaneSpec {
    return d[localIA = ia]
}

• We can then use these functions to describe what fields a method modifies and which remain the same in the following way:

...
ensures e == nil ==> d.Abs() == old(d.Abs()).UpdateIA(ia)
...
func (d *DataPlane) SetIA(ia addr.IA) (e error)

In order to prove these contracts, it might be helpful to use the approach I initially used -- i.e. only passing full permissions to the fields that are actually modified -- in the contract of an outline block within the "top-level method".

[henriman]

(router/io-spec-lemmas.gobra verifies successfully on my machine, so I'm not sure what the issue is with the pipeline.)

[jcp19]

@henriman are you using a different config for the router locally?

[henriman]

@henriman are you using a different config for the router locally?

It seems that the issue was due to me using a slightly outdated version of Gobra. With the most up-to-date version, I was able to reproduce and fix the issue (by adding an additional assert).