Hammer: Parser Combinators for C

Re:Hammer: Parser Combinators for C by nickpsecurity on Saturday July 25, 2015 @08:50PM (#9949662)

Great work by the LANGSEC crowd. My recent interest in parsers was those verified for correctness or security. So, they have security and a certain amount of correctness. A great next step would be combining it with work on formal verification of parsers or generators (see below). On top of that, ensure the subset could generate SPARK and/or CompCert-compatible C code to automate much of the rest of the problem.

TRX formally verified parser interpreter http://arxiv.org/pdf/1105.2576.pdf

Validating LR(1) Parsers http://gallium.inria.fr/~xleroy/publi/validated-parser.pdf

Verifying a parser for a C compiler http://gallium.inria.fr/~scherer/gagallium/verifying-a-parse...

[ Parent | on HN ]

Re:Hammer: Parser Combinators for C by maradydd on Sunday July 26, 2015 @12:13PM (#9951413)

Thanks! Those are all excellent papers. I am actually looking into formally verifying Hammer using Frama-C, but haven't gotten too far yet.

[ Parent | on HN ]

Re:Hammer: Parser Combinators for C by nickpsecurity on Sunday July 26, 2015 @10:24PM (#9953052)

Smart move. It's a good default far as work vs results tradeoff. I'll try to keep your project in mind when I review my collection of verification papers in case I see any little-known, C verification methods that might help.

[ Parent | on HN ]