[langsec-discuss] the frontier of decidability & TFP
edwin.brady at gmail.com
Fri Jun 12 08:55:27 UTC 2015
This seems a good moment to delurk :).
On 11/06/2015 23:54, travis+ml-langsec at subspacefield.org wrote:
> Although those links will require deep meditation I figured that
> perhaps it may interest other readers so I didn't just scrub this
> whole thing. The last link, TFP, is particularly exciting, as one
> could potentially have programs with specific construction, contracts,
> or proofs which could allow the user to execute them while limiting
> their powers. In essence, the burden of proof for security is shifted
> from the user to the program author.
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
More information about the langsec-discuss