[langsec-discuss] the frontier of decidability & TFP
sergey at cs.dartmouth.edu
Fri Jun 12 19:06:57 UTC 2015
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
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?
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!
>> Incidentally, not terminating or being misbehaved is a show-stopper
>> for executing in kernel mode, which would be a very efficient place to
>> langsec-discuss mailing list
>> langsec-discuss at mail.langsec.org
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
More information about the langsec-discuss