8 ms·

So most of the spec bugs I've come across don't have to do with English vagaries; they have to do with the reverse-engineering not being perfect. Converting the

So most of the spec bugs I've come across don't have to do with English vagaries; they have to do with the reverse-engineering not being perfect. Converting the nebulous concept of expected behavior into procedural text is hard, and there are bugs. So yeah, "implementation deviations" is usually the issue, but not really English ambiguity, at least with web specs. I put my pedant hat on when looking at proposed changes to web specs, and I believe the rest of the community does too :)

nickpsecurity 10y ago
Interesting. Thanks for the perspective.
gsnedders 10y ago
There have certainly been spec bugs that could be found from a formal specification, some of which are security related (most of the TLS bugs found by miTLS have been protocol bugs simply found as a result of encoding much of the semantics formally). That said, while I certainly have a fondness for formal specifications, I also always end up feeling like they have a lot of downsides. They're often very verbose and hard to skim, and they're also another language that anyone implementing the specification has to learn prior to implementing it (or they can just wing it, but then your formal specification is worth nothing!).
- nickpsecurity 10y ago
  Re specs downsides The wisdom from old days was to use relatively, simple, formal languages that were easy to train people on and use. B, Z, and TLA had good results plus lasted over time. The other thing was to do English spec, formal spec, and code side-by-side with each team looking for inconsistencies. The developers usually picked up the basics of the technique rather quickly but at least one specialist was always necessary to make first use go smoothly. So, that's still my recommendation. A subset of those, especially focusing on states and contracts, done in same fashion against English specs and clear code should take lower work than going all Isabelle, NuPRL, or PVS on a problem. Second application is also always easier. Reuse where possible helps as with code. So, some difficulties and training but probably easier than some frameworks, etc IT people learn today.
  - gsnedders 10y ago
    (As a disclaimer, for some context, I have only relatively passing experience with Z, and the majority of formal modelling of specs I've done is using CSP.) From when I've considered trying to formalise parts of the platform before, some of the things that often get hit very quickly are the fact that most of the web platform is defined in terms of sequences of Unicode code points, and ultimately any formalisation is going to have to deal with that (be it some complex parser—like HTML—or some simple validation of it matching a regular grammar). It has always seemed to me that to get much advantage you need to be able to programmatically assert statements about it (including, most obviously, pre-conditions are satisfied at all call-sites), but once you've gone from 2^256 to 2^1114112 characters you end up with such massive state explosion that even many symbolic tools start to struggle quickly. Now, maybe I've tried using the wrong tools, or maybe I'm structuring things wrong, but it'd be nice to have some way to do this.
    - nickpsecurity 10y ago
      Hmm. That's unusual situation. I've seen descriptions that sound similar in B data validation. For now, I'll just make a note of this comment to bring up when I next bump into formal methodists that might have answers.
      - gsnedders 10y ago
        Thanks! If you get an answer, please drop me an email (me@gsnedders.com), because I'd love to hear it.

nickpsecurity 10y ago

Interesting. Thanks for the perspective.

gsnedders 10y ago

There have certainly been spec bugs that could be found from a formal specification, some of which are security related (most of the TLS bugs found by miTLS have been protocol bugs simply found as a result of encoding much of the semantics formally). That said, while I certainly have a fondness for formal specifications, I also always end up feeling like they have a lot of downsides. They're often very verbose and hard to skim, and they're also another language that anyone implementing the specification has to learn prior to implementing it (or they can just wing it, but then your formal specification is worth nothing!).

nickpsecurity 10y ago
Re specs downsides The wisdom from old days was to use relatively, simple, formal languages that were easy to train people on and use. B, Z, and TLA had good results plus lasted over time. The other thing was to do English spec, formal spec, and code side-by-side with each team looking for inconsistencies. The developers usually picked up the basics of the technique rather quickly but at least one specialist was always necessary to make first use go smoothly. So, that's still my recommendation. A subset of those, especially focusing on states and contracts, done in same fashion against English specs and clear code should take lower work than going all Isabelle, NuPRL, or PVS on a problem. Second application is also always easier. Reuse where possible helps as with code. So, some difficulties and training but probably easier than some frameworks, etc IT people learn today.
- gsnedders 10y ago
  (As a disclaimer, for some context, I have only relatively passing experience with Z, and the majority of formal modelling of specs I've done is using CSP.) From when I've considered trying to formalise parts of the platform before, some of the things that often get hit very quickly are the fact that most of the web platform is defined in terms of sequences of Unicode code points, and ultimately any formalisation is going to have to deal with that (be it some complex parser—like HTML—or some simple validation of it matching a regular grammar). It has always seemed to me that to get much advantage you need to be able to programmatically assert statements about it (including, most obviously, pre-conditions are satisfied at all call-sites), but once you've gone from 2^256 to 2^1114112 characters you end up with such massive state explosion that even many symbolic tools start to struggle quickly. Now, maybe I've tried using the wrong tools, or maybe I'm structuring things wrong, but it'd be nice to have some way to do this.
  - nickpsecurity 10y ago
    Hmm. That's unusual situation. I've seen descriptions that sound similar in B data validation. For now, I'll just make a note of this comment to bring up when I next bump into formal methodists that might have answers.
    - gsnedders 10y ago
      Thanks! If you get an answer, please drop me an email (me@gsnedders.com), because I'd love to hear it.