Hacker News Reader

Comment by matthewdgreen | Hacker News Reader

It also means that formal verification needs to be part of the CI system, or at least "check that the code hasn't been changed in ways that violate the correctness guarantees" needs to be part of CI.

Doesn't do anything for this bug, which was an ASM issue. There's nothing you can do about this sort of bug except give people a better idea of the risks (e.g., make it clear that they can trade safety for performance.)

View on HN

Well, this issue was in the assembly, but it was not an assembly issue. It's interesting to think about how we could have encoded the assumptions in a machine-checkable way, because they are actually not unlike the assumptions of some formally verified components.

Here we had: 1) incomplete addition that had to be called with different points; and consequently 2) scalar multiplication that had to be called with a reduced scalar so the computation wouldn't wrap and add two equal points. I don't think we have the tools to encode (1), nor the fact that (2) satisfies (1). (2) maybe could have been encoded in the type system by accepting a ReducedScalar.

If you have to do things with type-based checking, presumably you can make two new types that are only ever output by one routine, something like ensureNotEqualPoints(A, B) -> (pointNotEqualTypeOne, pointNotEqualTypeTwo), err. Then you have one incomplete addition formula that takes in the two different point types. This doesn't protect you from calling it multiple times in a way that scrambles the types and breaks the invariant.

Formal verification with typechecking sucks and is very limited.

If you have a haskell style type system you can do such a thing and have the type system prevent you from calling things multiple times, eg:

  data P1 a
  data P2 a
  data PointNotEqual where
      | T :: P1 a -> P2 a -> PointNotEqual
  getP1 :: P1 a -> Point
  getP2 :: P2 a -> Point
  checkNE :: Point -> Point -> Maybe PointNotEqual
  (+) :: P1 a -> P2 a -> Point

Here when you are given a PointNotEqual, you don’t know what the type variable is, only that it’s the same between the two points. So you (ie the compiler) cannot prove that a P1 or P2 from a different call to PointNotEqual has the same type variable, so you can’t add them.

But these types also mean you need to do the check before every addition which defeats the point of the whole constant time thing, so the typechecking is still limited. And I guess you can’t do it in Go either.

Reply on news.ycombinator.com