Verify Secure Information Flow

[henriman]

I have started to verify SIF in my fork of VerifiedSCION. The relevant "main" branch is sif-io-spec (cf. #394).

---

Status

My approach was to go package by package, making each package verify on its own (thus, the annotations added so far are mostly to satisfy low control flow). When verification of a package necessitated changes to a previously verified package, I made sure to verify these changes; however, I may have missed some packages that were "indirectly" affected e.g. by changing an interface.

Note that, at the moment, one might need to use a "fix" for Gobra issue 948 in order to work on this project; see the discussion under this issue for a "quick-and-dirty" patch.

Packages successfully verified:

• Already merged into sif-io-spec: pkg/log, pkg/scrypto, pkg/private/serrors, private/topology/underlay, private/topology/underlay, router/bfd, private/topology, private/underlay/sockctrl, router/control, pkg/addr, private/underlay/conn, pkg/slayers/path/empty, pkg/slayers/path, pkg/slayers/path/epic, pkg/slayers/path/onehop

Remaining packages:

• pkg/experimental/epic: The package verifies successfully -- except for some issues with instability. Aside from these issues, there are a few more minor TODOs (not all of which can be addressed at the moment; one might consider merging this already and tracking the remaining TODOs/issues elsewhere); see PR #17.
• pkg/slayers: The package itself verifies successfully except for a ..._test.gobra file; furthermore, trying to verify pkg/slayers leads to Gobra complaining about some issues in other packages (not all of which can be addressed at the moment either). See PR #18.
• pkg/slayers/path/scion (on branch sif-pkg-slayers-path-scion).
  • This does not verify yet. Furthermore, this is in a bit of a messy state:
    • I merged sif-io-spec here just so that it doesn't crash when trying to verify pkg/slayers/path/scion.
    • This was originally based on an "old" branch for verifying pkg/experimental/epic which deviates significantly from what is now in sif-pkg-experimental-epic (cf. PR #17 on my fork). The annotations in pkg/experimental/epic (and in a few more places, such as in time) should be completely replaced in favor of the more up-to-date versions. I marked a few places in particular using appropriate TODOs in the code.
    • This still uses abstract Low predicates which are unsound (cf. PR #4)
  • I think it would be best to open a new branch (based on sif-pkg-experimental-epic or sif-pkg-slayers-scratch) and start the verification "from scratch" (though one can likely keep many of the existing annotations). This would probably be significantly more straight-forward than cleaning up the current state.
    • I left a few TODO comments for what needs cleaning up. Besides these, I would suggest wrapping many of the existing sensitivity contracts in IsLow functions, as the same pre- and postconditions are repeated often.
• router (no branch yet). I was not able to start verifying the router/dataplane itself. Note that verifying the dataplane requires moving the MAC assumption (Move "MAC assumption" deeper #399)
  • sif-io-spec already contains the IO spec (that I defined in my thesis).
  • However, some of these annotations might need to be adapted:
    • At the moment, my sensitivity annotations mostly refer to the abstract values (e.g. WriteBatch in the BatchConn interface in router/dataplane.go requires low(ioAbsPkts) instead of low(len(msgs)) && forall i int :: 0 <= i && i < len(msgs) && low(i) ==> low(msgs[i])). The only exception is in the declassification action Decl in verification/io/io-spec.gobra, which ensures that the array v.IO_decl_sigma is low and not its abstraction.
    • For convenience, and possibly for correctness, we might instead want to require/ensure that the concrete values are low, as we might not have low(<abstract value>) ==> low(<concrete value>)

Other verification efforts still in progress

• Moving the MAC assumption (cf. PR Move "MAC assumption" deeper #399)
  • Moving the MAC assumption necessitated changing the precondition of some methods in router/dataplane.go which should be tested for satisfiability. I have started adapting the tests in dataplane_spec_test.gobra in branch mac-assumption-dataplane-test; see PR Move "MAC assumption" deeper #399 for more information on this.
  • Except for the missing tests, this verifies successfully.
• Implement hyper functions (using branch fix-846 of Gobra). Due to Gobra issues 846, we were not able to implement IsLow functions yet. In PR #10 we start doing this. (However, due to Gobra issue 955, this can still not be done in many cases involving interfaces)
• Many of the dependencies and utils have not been verified on their own.

Besides these obvious TODOs and issues, the issues on my fork keep track of issues in already-merged packages that still need to be addressed.

---

For the general approach to working around Gobra issue 846 and abstracting sensitivity in general, see the (now closed) PR #4 (or my thesis).