[langsec-discuss] the frontier of decidability & TFP

travis+ml-langsec at subspacefield.org travis+ml-langsec at subspacefield.org
Thu Jun 11 22:54:16 UTC 2015


When we have problems that are undecidable such as the halting problem:

http://en.wikipedia.org/wiki/Halting_problem

The HRU problem:

http://en.wikipedia.org/wiki/HRU_(security)

Or Rice's Theorem:

http://en.wikipedia.org/wiki/Rice%27s_theorem

I wonder how frequently they are undecidable in practice, and
precisely what restrictions can one place on a program to make it
decidable.  I see there's some 

For example, I rarely encounter self-modifying code on "well behaved"
programs*, and their negative effect on halting decidability should be
obvious.

[*] Old-style signal trampoline and lazy-binding excepted;
    that's systems-level deep magic.
    http://sourceware.org/ml/gdb-patches/1999-q3/msg00053.html
    https://www.technovelty.org/linux/plt-and-got-the-key-to-code-sharing-and-dynamic-libraries.html

The idea is two-fold:

1) To precisely specify more than PDA and less than a TM which can
   still be analyzed.

2) To define the category of analyzable programs such that one can
   reason about them and assume the worst about programs which
   deliberately ("encourage the transparent, penalize the tricky").

Yay!  While writing/researching this question I may have found the
answers to it:

http://en.wikipedia.org/wiki/Termination_analysis

	[A] termination analysis is program analysis which attempts to
	determine whether the evaluation of a given program will
	definitely terminate. Because the halting problem is
	undecidable, termination analysis cannot be total. The aim is
	to find the answer "program does terminate" (or "program does
	not terminate") whenever this is possible. Without success the
	algorithm (or human) working on the termination analysis may
	answer with "maybe" or continue working infinitely long.

http://en.wikipedia.org/wiki/Total_functional_programming

	Total functional programming (also known as strong functional
	programming,[1] to be contrasted with ordinary, or weak
	functional programming) is a programming paradigm that
	restricts the range of programs to those that are provably
	terminating

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.

Incidentally, not terminating or being misbehaved is a show-stopper
for executing in kernel mode, which would be a very efficient place to
execute.
-- 
http://www.subspacefield.org/~travis/
"Computer crime, the glamor crime of the 1970s, will become in the
1980s one of the greatest sources of preventable business loss."
John M. Carroll, "Computer Security", first edition cover flap, 1977
-------------- next part --------------
A non-text attachment was scrubbed...
Name: not available
Type: application/pgp-signature
Size: 834 bytes
Desc: not available
URL: <https://mail.langsec.org/pipermail/langsec-discuss/attachments/20150611/34fbde0b/attachment.sig>


More information about the langsec-discuss mailing list