1. 15
  1.  

  2. 5

    A more accurate sub-heading would be that “no method” of verification caught Selfie, including formal verification. Cryptographer’s review, the secure coders, tests, formal verification… nothing that was applied caught it. Then, it’s not giving impression formal verification uniquely failed. It’s just elaborating on one of many failures.

    “At first glance, Selfie does indeed seem to fly in the face the unprecedented effort to formally verify TLS 1.3 as secure.”

    I prefer to be consistent. Teams like seL4 say the verification is that the implementation meets the spec, not absolutely secure. If we’re echoing this, we might say that some or many people thought TLS was secure due to formal verification. However, it was only verified against the spec that addressed attacks we understood. New attacks require new specs and tools with changes to the implementation. That simple.

    1. 3

      I prefer to be consistent. Teams like seL4 say the verification is that the implementation meets the spec, not absolutely secure. If we’re echoing this, we might say that some or many people thought TLS was secure due to formal verification. However, it was only verified against the spec that addressed attacks we understood. New attacks require new specs and tools with changes to the implementation. That simple.

      The author devoted the last third of the article to explaining this.

      1. 2

        One of the top priorities on my to-do list is a blog post reframing formal verification in the high assurance toolbelt. Right underneath that is reframing capabilities as automatically generated, finely grained sandboxing.

        1. 1

          That fits a lot of uses for capabilities. Developers can learn advanced stuff later on. Is there a brief summary of the reframing for formal verification? And do submit it here when done. :)