Hello Edwin,
I think this is a very promising approach and a very important
distinction. As we argue that verification should focus on parsers and
transducers, non-terminating parsers or transducers should be naturally
suspect. Also, there is a clear connection between unexpected/emergent
computation models (a.k.a. "weird machines") using unanticipated state and
the functional programming's mantra of making such state unrepresentable :)
I think it would naturally combine with the that emerged from the Crema
work, that of programming recognizers and transducers in a language with a
deliberately limited computation model. The linking boundary thus becomes
the type enforcement boundary, and, possibly, a systems-backed isolation
boundary, as well as a natural boundary of specification for the rest of
the program.
As we begin planning for the next year's LangSec event, perhaps we
could persuade you to join us and do a presentation and/or a tutorial on
these uses of Idris?
Thank you,
--Sergey
On Fri, 12 Jun 2015, Edwin Brady wrote:
This is one of the application areas we have in mind for Idris
(http://www.idris-lang.org/) which is a language that supports total
functional programming (optionally, by flagging the fragments of
programs you wish to be total).
I'm not particularly expert on security, sadly, but the gist of the idea
is to write a communication protocol as a type and verify by type
checking that your implementation satisfies that protocol. There's an
early attempt at https://github.com/edwinb/protocols, which has stalled
a bit lately but the README should give some idea of what's going on.
Totality checking is important here: it's the difference between "My
program is guaranteed to produce a result of this form" and "If my
program terminates and doesn't crash, then the result will be of this form".
Idris itself needs a fair bit of polish for this sort of thing to work
well, but we'll know better which bits we need to fix by having a go at
solving interesting problems!
Edwin.
Incidentally, not terminating or being misbehaved is a show-stopper
for executing in kernel mode, which would be a very efficient place to
execute.
_______________________________________________
langsec-discuss mailing list
langsec-discuss@mail.langsec.org
https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
_______________________________________________
langsec-discuss mailing list
langsec-discuss@mail.langsec.org
https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
_______________________________________________
langsec-discuss mailing list
langsec-discuss@mail.langsec.org
https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
