Hacker News Reader

Comment by layer8 | Hacker News Reader

This is the important takeaway:

> The second, more interesting lesson is that while assumptions might be valid now, they aren’t guaranteed to be valid in the future, after the code is refactored or reused over the years. It’s important to minimize assumptions and clearly document the remaining ones, as much as possible into the API or type system, and otherwise in high-level comments.

A lot of software engineering lessons can be reduced to “minimize assumptions and dependencies”. This includes the assumption that assumptions won’t change in the future.

View on HN

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.)

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