Evan, Thanks, this is spot on. Finding the right question to answer (balancing power and practicality) is exactly what I was after. On May 27, 2014 12:05 PM, "Evan Sultanik" < evan.sulta...@digitaloperatives.com> wrote:
> On Mon, May 26, 2014 at 08:55:59PM -0700, Paul Burchard wrote: > > What are known results mitigating the basic computer science problem that > > it's normally expensive or impossible to answer the fundamental language > > security question: what might some code do with the powers it's given? > > It depends on what question you're ultimately trying to answer. While > answering the question, > > "What might this code do *under all possible inputs* with the > powers it is given?" > > is usually intractable, if not undecidable, it is important to > remember that solving the "dual" of the problem is often much easier: > "Does there exist an input that causes this code to [perform a > specific behavior]?" In other words, it is often much easier to find > *at least one* certificate (i.e., input) that exercises a certain > desired behavior (e.g., halting). If there are only a limited number > of behaviors about which one is concerned, this approach can often be > tractable, if not even efficient. > > I may be side-stepping your actual question here, but my point is that > it can often be fruitful to constrain the set of inputs as opposed to > constraining the language. > > There are already many program analysis techniques [1,2] like concolic > execution that provide an "oracle" for answering questions like, "Does > there exist a set of inputs that causes [a specific pointer] to be > used after it is freed?" Constraint solvers [3,4] allow us to query > for inputs that exercise almost arbitrarily complex behaviors, many of > which are tractable to solve. There has also been some recent success > at using machine learning to classify the behavioral characteristics > (as opposed to logical flow) of black-box binaries [5]. Liveness and > deadlock can also be relatively efficiently determined using solely > static analysis and model-checking [6,7]. > <shameless-self-promotion>My employer, Digital Operatives [8], has > developed a static analysis tool for detecting liveness and performing > arbitrary constraint satisfaction and optimization on > LLVM/IR.</shameless-self-promotion> > > Now, back to your actual question. It's clear that > non-Turing-complete languages can be useful. For example, > Hofstadter's old BlooP [9] language can do useful computations like > computing factorials, however, it explicitly disallows unbounded > (infinite) loops, so the halting problem is decidable for it. A > somewhat more recent---but still old---example is the CHARITY > programming language [10], which uses category theory [11] to > guarantee termination. Finally, you probably want to read the Hume > Report [12] which describes a hierarchical system architecture that > provides layers of non-Turing-completeness for security. > > - Evan > > [1] http://llvm.org/pubs/2008-12-OSDI-KLEE.html > [2] http://s2e.epfl.ch/ > [3] http://chicory.stanford.edu/PAPERS/STP-ganesh-07.pdf > [4] http://z3.codeplex.com/ > [5] http://www.blackhat.com/us-13/briefings.html#Saxe > [6] http://www.cs.utexas.edu/~shmat/shmat_csf09.pdf > [7] > http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf > [8] http://www.digitaloperatives.com/ > [9] http://en.wikipedia.org/wiki/BlooP_and_FlooP > [10] http://pll.cpsc.ucalgary.ca/charity1/www/home.html > [11] http://en.wikipedia.org/wiki/Category_theory > [12] http://www-fp.cs.st-andrews.ac.uk/hume/report/hume-report.pdf > > _______________________ > Evan A. Sultanik, Ph.D. > Chief Scientist > Digital Operatives, LLC > Mobile: +1 215 919 7234 >
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
