This reminds me of the goals of the Crema programming language [1] I recently presented at the IEEE S&P LangSec workshop [2]. It was a study into "given a provably terminating language, what can you *do* with it". The first step (completed) was the build such a language that is easy enough to use and learn that the average software engineer would feel okay being tasked to write something in it. We also gathered some empirical evidence that there were verification wins.
The second step (in progress) is to identify what % of an "average" software project requires unbounded computations (i.e. server listen loop, REPL or OS scheduling loops) versus what parsers/transducers can be run safely in sub-TC space (USB drivers, file parsers, etc..). Hopefully this work will be published within a year. It is intuitively clear that parsing should be a terminating computation, and if it is not, it speaks strongly to a format specification that is too vague or inappropriately scoped [3]. [1] http://ainfosec.github.io/crema/ [2] http://spw15.langsec.org/abstracts.html#ver [3] http://spw14.langsec.org/papers/pdfparser-report.pdf -- Jacob On Fri, Jun 12, 2015 at 2:55 AM, Edwin Brady <edwin.br...@gmail.com> wrote: > 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 >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
