The Bugs We Have to Kill [pdf] | Hacker News Reader

The Bugs We Have to Kill [pdf]

usenix.org

47 pointsvezzy-fnord22 comments

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

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.

To the application, there's no such thing as TCP packet length. Is there a TLS packet length?

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.

Something, something, the LISP guys have known this forever something, something.

edit: This article almost perfectly articulates why I'm so furious at the entire web-as-a-platform movement. If you want general computation lets develop a platform for it that is isolated and doesn't try to turn what should be nothing more than text into a full blown programming language. The browser should be (good luck getting it back there) for viewing and retrieving data, not executing that data.

> The browser should be ... for viewing and retrieving data, not executing that data.

i'm genuinely interested in what a modern version of that would look like.

recently i watched a 1992 interview [0] with brewster kahle in which he described WAIS (wide area information server) [1].

aside: i've not used WAIS, nor do i feel it is the way forward.

my understanding is that WAIS provided a client-side interface to a directory of servers. it also seems the presentation of content was simple: mostly text, but some images and video, too. this appeals to me because after more than 20 years on the web i struggle to remember what it was like when (or even if) the majority of pages i visited were focused on delivering pure content.

don't get me wrong -- i'm fortunate to have access to the web and a way to search for information -- but i'm becoming increasingly frustrated with the quality of today's content.

i'll concede SERP SPAM is a hard nut to crack, but that doesn't stop me from cringing every time i click on a dodgy question/answer aggregation site or some wholesale ripoff of another site [2].

and less dodgy but arguably more frustrating are legitimate publishers who modify their content presentation strategy based on google algorithm updates. for example, i can't tell you how many times i've searched for a simple recipe but the top SERP was a slideshow instead of a simple recipe i could print out and place on my counter top.

lastly, over the past 20 years it seems like primary content has become a secondary citizen on the web. when i visit SERPs today it feels like i'm less likely to be presented with what i actually searched for. instead, i'm increasingly bombarded with "SIGN UP NOW!" mortars .. erm modals .. and the presentation of the content i searched for feels more like Dahala Khagrabari [3] than the main reason for my page visit.

one might read the above and conclude i'm a bitter luddite. quite the contrary, i feel blessed to be alive and am optimistic (mostly ;) WRT the future of IT. however, i am concerned with (what seems like) this generation's tendency to favor presentation over information. the older i get the less patience i have for popups/modals, slideshows, and pictures-because-google-likes-pictures; just gimme my goddamned information already.

so. i'd really like to see a dumb client-side app that gives me only what i want to see. i've tried lynx/w3m-emacs/etc. but JavaScript ruined that effort. keen for alternative suggestions :)

[0] https://archive.org/details/brewster_kahle_interview_1992

[1] https://en.wikipedia.org/wiki/Wide_area_information_server

[2] http://stuccy.com/ is a wholesale ripoff of stackoverflow. (note: i don't recommend visiting this site; who knows what they're up to.) i've emailed SO, whose response was essentially this:

> Please note, bringing these sites into compliance (or getting them to no longer serve our content) is often a long and arduous process. You may not see immediate results. However, rest assured that we're working on it.

[3] https://en.wikipedia.org/wiki/Dahala_Khagrabari

This is why, on mobile devices, where you have a new kind of UX, almost everything needed a native UI implemented as an app. The Web is a nice programmable hypertext system. Sometimes it's worth pushing the limits of that. But not for everything.

If I understand it correctly, it demands to use simpler input languages, namely languages you can parse with a context-free grammar (in CS speak LL(k) or even better SLL(k)). To clarify, it is not about so much about how the programmers implements it (parser generator, combinator, or hand-coded), but more about what languages we specify.

Well, how many languages (or data formats) are SLL(k)? SQL is not, for example. A context-free grammar for SQL accepts "INSERT INTO example (a, b) VALUES ('test');". You need an additional check to find that you specify two columns to insert, but provide only one value.

This is common practice: Have a context-free grammar which accepts a superset of the actual language and filter it afterwards. Maybe you can fit the grammar more to the language, but it becomes quite ugly and big then. I don't think it is a good idea that we try to avoid the filter-afterwards and use big grammars, which we implement with shiny verification tools.

Hence: languages with a lexer pass followed by a parser pass.

I was mostly talking about the semantic analysis pass after the parser pass. Type checking, name binding, etc.

You are correct that the lexer pass allows you to expand a language despite the use of a context-free grammar in the parser. Significant whitespace lexed as indent/dedent tokens is a common example.

Getting parsers right will always be important, since they're often "on the front lines" exposed directly to untrusted input and thus the easiest code to manipulate. That includes making sure they can't be made to crash, eat up unbounded amounts of memory, or return semantically invalid to the next layer of the program. But in most cases, it shouldn't require ensuring they can't be made to execute arbitrary code, because we should be writing them in languages that do not allow for such vulnerabilities. Over the years, the arguments against doing so are getting weaker as the costs of not doing so get bigger. Soon there will be no excuse.

There is another bug I think we must get rid of: generating HTML using printf techniques.

Not only we should have verified parser, but also verified serializers.

http://m1el.github.io/printf-antipattern/

(EDIT: I know it is badly written and there are errors, but, I'm looking forward to rewriting it)

The paper seem closely related to another paper by all the three authors and the late Len Sassaman, titled "The Halting Problems of Network Stack Insecurity".

http://langsec.org/papers/Sassaman.pdf

Why the focus on context-sensitivity? You can perfectly well validate a (restricted subset of) HTML with a regex - regexes are in fact very good at input sanitization. Parsers are dangerous because formats have exponentially many edges for you to get cut on. This is the case for regular, context-free, and worse formats.

What subset of HTML are you talking about here? HTML is not regular. Regexes can't do recursive things, such as matching opening and closing tags, and abusing regexes to sort of match HTML is generally considered a terrible idea.

There is a conceptual version of HTML that's non-regular, but HTML as used in practice is regular, because the standard allows parsers to impose a maximum nesting depth, and all browsers that I know of do so (e.g. Webkit limits to 512). Every finite language is regular, so HTML with a finite tag-nesting depth is regular. Therefore you could in principle parse the subset of HTML recognized by Webkit using a regular expression.

It's impractical and error-prone to do so, of course, but that's not a computability issue. You could write a compiler, if you really wanted to, that took a context-free grammar plus an integer specifying maximum production depth, and mechanically converted it to an FSM or regex. Therefore I think the article is barking up the wrong tree with computability; the issue isn't what's computable by a finite vs. pushdown automaton, but that parsing nested data structures with regexes is virtually impossible to do correctly.

I think you are technically correct, but your proof contains a non-sequitur: limiting tag-nesting depth doesn't limit the size of a string accepted as HTML, because the textual contents of any tag (or an attribute, or sequenced rather than /nested/ tags) may be of unlimited length.

It's true anyway. The limited depth means it has a finite number of states, regardless of the length, and that's all you need for it to be regular.

But this is a technicality and it should in no way indicate that a regex for HTML would be a good idea.

The reason I think it's useful to note, even though you would not in practice parse it that way, is that in my opinion it better points to why parsing HTML with regexes is a bad idea. It would be possible to do so with a giant regex, but there are two problems: 1) manually writing regexes to parse nested data structures is bug-prone; and 2) finite-automaton size scales very badly with the choice of nesting limit, which is more of a complexity rather than computability issue.

Say you had a recursive data structure with a very small maximum nesting depth, like 5. Should you use a regex then? I would argue still no: there's no computational problem, but writing a correct regex to do so is still bug-prone. At least, writing one manually is. In the case of small finite nesting depths there might occasionally be reasons to mechanically compile something that looks more like EBNF to a DFA or NFA. But something else might well be better. At that point it's just an efficiency question.

Regexes can't do recursive things

Basic regular expressions cannot, but regexes actually can. PCRE pioneered the technique AFAIK, and it later spread to Perl, Python, Ruby and other runtimes. Perl has this feature called lazy regular subexpressions which can be used to evaluate Perl expressions upon matching a subexpression, thus giving you the ability to recurse.

So, yes, some implementations of regular expressions are Turing complete because they run arbitrary code, but that is rather the opposite of a way to make parsers safer.

On that note, once you can run arbitrary functions on your matches, you could match /.*/ and then the function you run is html5lib.parse. Is that still a regular expression?

Of course using regexes on general-purpose HTML is a bad idea. Using regexes to ensure the sanity of a restricted markdown converter isn't, especially if you want to err on the side of conservatism.

Reply on news.ycombinator.com