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
pgpBpoKTFHEzc.pgp
Description: PGP signature
_______________________________________________ langsec-discuss mailing list langsec-discuss@mail.langsec.org https://mail.langsec.org/cgi-bin/mailman/listinfo/langsec-discuss
