Hi all, This seems a good moment to delurk :). On 11/06/2015 23:54, travis+ml-lang...@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! 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
