[langsec-discuss] Basic results?
paulburchard at gmail.com
Tue May 27 16:45:57 UTC 2014
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.sultanik at 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 . 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 , has
> developed a static analysis tool for detecting liveness and performing
> arbitrary constraint satisfaction and optimization on
> Now, back to your actual question. It's clear that
> non-Turing-complete languages can be useful. For example,
> Hofstadter's old BlooP  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 , which uses category theory  to
> guarantee termination. Finally, you probably want to read the Hume
> Report  which describes a hierarchical system architecture that
> provides layers of non-Turing-completeness for security.
> - Evan
>  http://llvm.org/pubs/2008-12-OSDI-KLEE.html
>  http://s2e.epfl.ch/
>  http://chicory.stanford.edu/PAPERS/STP-ganesh-07.pdf
>  http://z3.codeplex.com/
>  http://www.blackhat.com/us-13/briefings.html#Saxe
>  http://www.cs.utexas.edu/~shmat/shmat_csf09.pdf
>  http://www.digitaloperatives.com/
>  http://en.wikipedia.org/wiki/BlooP_and_FlooP
>  http://pll.cpsc.ucalgary.ca/charity1/www/home.html
>  http://en.wikipedia.org/wiki/Category_theory
>  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
-------------- next part --------------
An HTML attachment was scrubbed...
More information about the langsec-discuss