[fsddfsdfssdf]

While I can see the shortcomings of C and generally don't recommend it for new projects I don't see this particular bug as a good example of something Rust's borrow checker or some other language's type system will catch. I don't think even static analyzers can catch this.

It's basically something like this:

original: DoTheThing()

new: DoTheThingSlightlyDifferentButKeepMyCredentialsAlive()

fix: DoTheThingSlightlyDifferentButDoInFactNOTKeepMyCredentialsAlive()

In my experience a substantial portion of gnarly bugs come down to a violation of a high-level system invariant and those do not strike me as something that can be automated. Even with something like Lean you can prove your program satisfies certain properties but you need to have thought about those properties in the first place. The proof doesn't discover the invariant for you.

If you'd had thought about the relevant security property you could have written a regression test for it which is not hard. IMO the really hard part isn't expressing the implementation safely, but it's the realization that this was a property the implementation needed to preserve.

[estebank]

This is in effect a state machine, and when you have a type system more complex than C's you can encode state transitions in the type system (either by having state transitions explicitly return a new return type or by using sum types). You still need to architect the system to encode the invariants in types. No language will fix all logic bugs for free. But you can leverage language features to reduce their number.

[fsddfsdfssdf]

> You still need to architect the system to encode the invariants in types.

That's the problem though, right? If it's pointed out we all agree the "do not keep credentials alive" is a property that should hold and we can leverage whatever the environment offers to help preserve it. I fully agree modern languages have amazing support for this, but in C you can still run tests. Let's just say I don't think the language's inability to express logic of this kind held all those involved back from testing for it. I personally find "we just didn't think of it" much more likely.

That said, I am not a fan of C and recommend leveraging whatever fantastic modern tooling is available to you.

[J_Shelby_J]

Like set an generic marker struct IsEncrypted<T> where T is yes or now and only allow its state to change when proven and then write the shutdown function to only take the yes variant?

[estebank]

Yes, that would be one way of doing it. You can model off of the Typed Builder pattern:

  struct Builder<const A: bool, const B: bool> {
    a: Option<u32>,
    b: Option<u32>,
  }
  struct Val {
    a: u32,
    b: u32,
  }
  impl<const B: bool> Builder<false, B> {
    fn set_a(self, a: u32) -> Builder<true, B> {
      Builder {
        a: Some(a),
        b: self.b,
      }
    }
  }
  impl<const A: bool> Builder<A, false> {
    fn set_b(self, b: u32) -> Builder<A, true> {
      Builder {
        a: self.a,
        b: Some(b),
      }
    }
  }
  impl Builder<true, true> {
    fn build(self) -> Val {
      Val {
        a: self.a.unwrap(),
        b: self.b.unwrap(),
      }
    }
  }

This won't work for everything, but it is a pattern that I find useful to ensure that things can't happen out of order.

[bbminner]

I agree re Rust vs C - this is not (only) a language issue. What would (roughly) the invariant be here?

In another thread comment below i argue that maybe the system (OS) itself is so complex that it lacks clear contract / the contract evolves too quickly over time (as other parts of the code need to change the given piece of code to extend it to their use case) and that defies clear encoding?

Or we lack easy enough means to describe specs? I tried reading jepsen spec earlier today and despite it being an "integration test" of sorts, it is far from "simple".

Can an entire OS or a system of comparable complexity be decomposed into objects simple enough that their entire intended behavior (with all edge cases) can be explained in a paragraph of human text + half a screen of dense behavioral "spec" - if i do X and do Y, Z should come out / hold _no matter what happens in-between_. Or that's what asserts + fuzzing is effectively supposed to do? Is there a clear distinction between invalid input and failed invariant in typical C code? I guess error code vs seg fault?