[langsec-discuss] the frontier of decidability & TFP

Sergey Bratus sergey at cs.dartmouth.edu
Fri Jun 12 19:06:57 UTC 2015


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 at mail.langsec.org
>> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>>
> _______________________________________________
> langsec-discuss mailing list
> langsec-discuss at mail.langsec.org
> https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
>


More information about the langsec-discuss mailing list