4 ms·

Some things about this are a mess. For one, they claim that CompCert doesn't have a formally verified C parser, but it does, as of 2014. Instead of citing the

by munin 11y ago

Some things about this are a mess. For one, they claim that CompCert doesn't have a formally verified C parser, but it does, as of 2014. Instead of citing the CompCert release page, they cite a paper written in 2011 that says that CompCert does not have a verified parser. The concerns about proofs in Hoare logic (they also don't get the notation for Hoare triples right...) are mis-guided as well. The way that type checking works in strong, statically typed languages, the conditions they worry about don't arise by construction. They say that isn't possible, but it totally is possible and is done in projects like CompCert, bedrock, and some Haskell frameworks. Also, they say that Heartbleed is a parser error. I don't see how, because the heartbeat message is perfectly well formed, the size of the data requested is larger than the size of the buffer. How is this a parser error? The patch wasn't a change in parser behavior either, so...

jbangert 11y ago
Verifying length fields is absolutely a parser issue. Heartbleed and similar bugs arise from the fact that the length is encoded (at least) twice -- once, in the explicit length field, once implicitly in the length of the transmitted data (i.e. the TCP packet length). If multiple copies of the same redundant information are not identical, then that is definitely a case of invalid input. I try to address this class of parser vulnerability with my Nail parser generator (OSDI '14 , github.com/jbangert/nail ), which is inspired by Meredith's hammer.
- heinrich5991 11y ago
  To the application, there's no such thing as TCP packet length. Is there a TLS packet length?
  - richm44 11y ago
    There's a length field in a TLS record and also one in the heartbeat message itself. Heartbleed happened when the length field of the heartbeat message was longer than the length of the tls record.

by munin 11y ago

jbangert 11y ago

Verifying length fields is absolutely a parser issue. Heartbleed and similar bugs arise from the fact that the length is encoded (at least) twice -- once, in the explicit length field, once implicitly in the length of the transmitted data (i.e. the TCP packet length). If multiple copies of the same redundant information are not identical, then that is definitely a case of invalid input. I try to address this class of parser vulnerability with my Nail parser generator (OSDI '14 , github.com/jbangert/nail ), which is inspired by Meredith's hammer.

heinrich5991 11y ago
To the application, there's no such thing as TCP packet length. Is there a TLS packet length?
- richm44 11y ago
  There's a length field in a TLS record and also one in the heartbeat message itself. Heartbleed happened when the length field of the heartbeat message was longer than the length of the tls record.