In Defense of Erlang: Through Magic of Offence(drive.google.com)
drive.google.com
In Defense of Erlang: Through Magic of Offence
https://drive.google.com/file/d/0Bz8Lmg2kodQiRXYwWVpGNXQtdG5hNG5GaDFFNF9UNXp4UXo4/view
7 comments
Pretend model checking?
Pretend 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.
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.
The slides were previously discussed on the Erlang mailinglist.
http://erlang.org/pipermail/erlang-questions/2016-June/08941...
http://erlang.org/pipermail/erlang-questions/2016-June/08941...
> All user written code is call-back based, reducing code complexity
I think this line deserves further explanation. (I wish people would just post the video of a talk instead of slides, they are often devoid of important context).
I think this line deserves further explanation. (I wish people would just post the video of a talk instead of slides, they are often devoid of important context).
Erlang programs are typically structured around OTP-like style. In this style an executing process consists of an "upper" half, written by the user as a module of callback hooks. And a "lower" half which is reused in all components. The lower half usually doesn't "trust" that the upper half is doing things correctly.
Furthermore, Erlangs core is functional, so data is by default persistent which makes it harder for code to do "nasty" things to other parts of the code.
From a correctness perspective it makes it harder for code to mess up. From a security perspective correct code with hard error constraints is safe, leading to controlled process crashes with no memory corruption.
Of course it is no panacea, but it goes a long way toward making systems safe.
Furthermore, Erlangs core is functional, so data is by default persistent which makes it harder for code to do "nasty" things to other parts of the code.
From a correctness perspective it makes it harder for code to mess up. From a security perspective correct code with hard error constraints is safe, leading to controlled process crashes with no memory corruption.
Of course it is no panacea, but it goes a long way toward making systems safe.
the erlang odbc module will also let you overwrite the heap if you aren't careful. it lets you specify a string size for query params and if you pass in a binary/list that is larger than the string size it will just corrupt the heap. if you are not validating client input this can be remotely exploitable. :/
This sounds pretty bad, has it been reported?
Just want to shoutout to the Nerves Project, which is working on creating a platform for Elixir on embedded systems:
http://nerves-project.org/watch/
http://nerves-project.org/watch/
> High security potential
What is that supposed to mean?
What is that supposed to mean?
ps4fanboy(2)
"Only" exploit developer?
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.