[langsec-discuss] the frontier of decidability & TFP
jacob at jacobtorrey.com
Fri Jun 12 15:39:22 UTC 2015
This reminds me of the goals of the Crema programming language  I
recently presented at the IEEE S&P LangSec workshop . 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 .
On Fri, Jun 12, 2015 at 2:55 AM, Edwin Brady <edwin.brady at gmail.com> wrote:
> Hi all,
> 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
> 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
> > 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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss