5 ms·
Whoa whoa whoa. "Only" exploit developer? https://github.com/zv/otp https://github.com/zv/otp I was writing the fuzzing machinery for the BEAM instruction de
by ZephyrP 10y ago
Whoa whoa whoa.
"Only" exploit developer?
https://github.com/zv/otp https://github.com/zv/otp
I was writing the fuzzing machinery for the BEAM instruction decoder AND EPMD while you were ... doing much more impressive stuff.
Besides paragons of industry like myself, The "CUTER" guy (known by his friends as "Greek Fire") has done considerable work in manually verifying and pretend model checking large swaths of the Erl OTP code, despite being less "vulnerable" than the biffer or port-mapper (for example), DOES happen to comprise the vast majority of the OTP code base.
Other people have done admirable work in reviewing OTP, patching remotely exploitable holes and advancing our security posture. Unsurprisingly this breed of hacker doesn't bother registering a catchy domain name with a dope live stunt-hacking demo to Wired.
This is to say you've never heard of them.
- cgag 10y agoPretend model checking?
- ZephyrP 10y agoPretend model checking is an exciting new field born from frustrations with actually model checking large amounts of code that accepts somewhat arbitrary inputs and uses (large) loops. After enough neologisms like 'symbolic execution' and 'program synthesis' the distinctions between the various terms-of-art break down for laymen like myself and it all blurs together into some vague guarantee about software behavior. In Aggelos Giantsios's (CUTER's) case, this means writing your own stuff. Everywhere else, this means writing a TLA+ specification for your favorite component of the term protocol, some implementation environment and "slapping on the TLAPS". This has the unfortunate property of only model checking a model that the implementer THINKS the program behaves in (many 'model checking' efforts fit into this camp). Those who are truly serious about verification have a Maude<->ACL2 of the resulting assembly or try to check for symbolic constraints with KLEE. Those who are even MORE serious (usually on philosophical grounds) have a host of approaches I couldn't even tell you about.