4 ms·
Wuffs seems fascinating and I really wanted to like it. But when I look at the code for the JSON decoder it seems so low level, and full of places for bugs to
by chubot 6y ago
Wuffs seems fascinating and I really wanted to like it. But when I look at the code for the JSON decoder it seems so low level, and full of places for bugs to hide. JSON is a pretty simple spec and this obscures it (although to be fair it's also handling UTF-8).
https://github.com/google/wuffs/blob/main/std/json/decode_json.wuffs https://github.com/google/wuffs/blob/main/std/json/decode_js...
Yes it prevents buffer overflows and integer overflow, but it can't prevent logical errors.
I'd rather see efficient code generated from a short high level spec, not an overwhelming amount of detail in a language verified along a few dimensions.
---
Logical errors in parsing also lead to security vulnerabilities. For example, here is an example of parser differentials in HTTP parsing:
https://about.gitlab.com/blog/2020/03/30/how-to-exploit-parser-differentials/ https://about.gitlab.com/blog/2020/03/30/how-to-exploit-pars...
The canonical example of this class of bug is forging SSL certificates to take advantage of buggy parsers, but I don't have a link handy. There should be one off of https://langsec.org/ https://langsec.org/ if anyone can help dig it up.
Again, this has nothing to do with buffer or integer overflows.
(aside: while googling for that I found the claim that mRNA vaccines work by parser differentials: https://twitter.com/maradydd/status/1342891437537505280?lang=en https://twitter.com/maradydd/status/1342891437537505280?lang... If anyone understands that I'd be curious on an opinion/analysis :) )
At the very least, any language for parsing should include support for regular languages (regexes). The RFCs for many network protocols use this metalanguage, and there's no reason it shouldn't be executable. They compile easily to efficient code.
The VPRI project claimed to generate a TCP/IP implementation from 200 lines of code, although it's not really a fair comparison because it hasn't been tested in the wild: https://news.ycombinator.com/item?id=846028 https://news.ycombinator.com/item?id=846028 .
Still I think that style has better engineering properties. Oil's lexer, which understands essentially all of bash, is generated from a short source file
https://www.oilshell.org/release/0.8.8/source-code.wwz/frontend/lexer_def.py https://www.oilshell.org/release/0.8.8/source-code.wwz/front...
which generates
https://www.oilshell.org/release/0.8.8/source-code.wwz/_devbuild/tmp/osh-lex.re2c.h https://www.oilshell.org/release/0.8.8/source-code.wwz/_devb...
which goes on to generate 28,000 lines of C code. It's short, but it really needs a better regex metalanguage to be readable: https://www.oilshell.org/release/latest/doc/eggex.html https://www.oilshell.org/release/latest/doc/eggex.html
A large part of JSON can be described by regular languages, and same with HTTP, etc.
-----
edit: An re2c target for wuffs could make sense. The generated code already doesn't allocate any memory, although it uses tons of pointers which could be dangling.
And in fact that was a problem Cloudflare, which sprayed the user data of their customers all over the Internet back in 2017: https://en.wikipedia.org/wiki/Cloudbleed https://en.wikipedia.org/wiki/Cloudbleed
That was with Ragel and not re2c, which perhaps has a more error prone API.
- summerlight 6y ago> I'd rather see efficient code generated from a short high level spec This is a holy grail for many PL researchers, but I don't think that there's any languages that reached this level of sophistication with expressiveness/practicality enough for production usages. At least with the status quo, you will probably need to write a massive amount of formal proofs if you want logical correctness, even with deceivingly simple specifications.
- chubot 6y agoIt doesn't have to be the same metalanguage for every program. You can write your own code generators adapted to the specific problems. They should have a "pit of success", and the knowledge of the domain is used to ensure that. There are few research-level issues here; it's just good engineering. The 0% or 100% mindset is bad engineering. You want something that's short, and that you can explain to other people, and that other people can write an independent implementation of. If the proof is 10x longer than normal code, and it's written in a metalanguage that the relevant people don't know, then it's not very useful. Proofs are not guarantees. CompCERT has had logic bugs despite being written in a formal language. (It does reduce the number of bugs drastically in general, but it's also an extremely expensive technique, and not what I'm advocating.) There are no guarantees in engineering, just good practices. Groveling through bytes one at a time in imperative languages is not an ideal engineering practice, even if the imperative language comes with more guarantees than most.
- dmitriid 6y ago> JSON is a pretty simple spec a Yet there are no proper implementations because it's too simple, sometimes ambiguous, and there are several standards. JSON parsing is a minefield, http://seriot.ch/parsing_json.php http://seriot.ch/parsing_json.php
- chubot 6y agoJSON is simple compared to any textual format and many binary formats. Compare it with HTTP 1.1, 2, 3, or say Apache Arrow. JSON is a compromise, and specifies only syntax, without semantics, and without an API. But I think that was a good tradeoff compared to say XML syntax, schemas, and APIs like SAX and DOM. You can build a lot of stuff on top, and people have.