4 ms·

Well, take things that way: if your language is not Turing-complete, you could lock things down so that no crazy stuff happens, and prove that there is no way t

Well, take things that way: if your language is not Turing-complete, you could lock things down so that no crazy stuff happens, and prove that there is no way to bypass the security --assuming this problem is decidable, which can be the case if the language is not Turin-complete, but is hopeless otherwise. So it's a bit like saying "well, both are dogs so both can bite", when one is well-trained and leashed, and the other is loose and raging.

radarsat1 11y ago
Can you give an example of how the halting problem allows one to make it impossible/difficult to detect malicious code? I sort of get what you are saying, that Turing completeness makes analysis more difficult, but I still don't see what it has to do with security.
- yk 11y ago
  Well, if you can somehow inject arbitrary code, then you can inject an infinite loop. So a program will only halt on all inputs if you can not inject an infinite loop.
  - radarsat1 11y ago
    Sure.. so how is an infinite loop a security vulnerability?
    - JadeNB 11y ago
      If you are performing data processing on user-supplied inputs (as online compilers do), then an infinite loop can amount to a DoS attack.
    - yk 11y ago
      The argument is the other way around, if a program halts on all inputs, then there is no possibility to inject arbitrary code. ( There may still be important security vulnerabilities, but there are some limits. Consider a debugger that executes the first 10 000 operations of a program, it would halt, but 10 000 operations is a lot of space to do something malicious.)
    - coldtea 11y ago
      Security doesn't end with "privilege escalation". "Killing" (DoS) a system is also an attack.
- yaps8 11y ago
  The halting problem makes it impossible to consistently answer the question "Will this instruction be executed ?" This is why you can't know if the code is malicious : you can't (always) infer meaningful properties about the code (Will it write something on the disk ?...).
  - JadeNB 11y ago
    > The halting problem makes it impossible to consistently answer the question "Will this instruction be executed ?" In fact, Rice's theorem says that it's impossible more generally to answer any question about arbitrary code—so no work-arounds like "OK, I can't tell if a particular instruction is executed, but I can just test whether this program is 'safe'" (say, performs no I/O).
    - 9mit3t2m9h9a 11y ago
      And the reason why you cannot check that the program performs no I/O is because you cannot check if the I/O instructions are behind an infinite loop or an impossible condition or not. It is definitely easy to verify that a program has no references to I/O instructions. This will reject programs like «if(false) then write("Hello")», so it is not a violation of Rice theorem (functionally equivalent programs are not treated in the same way). But you don't need to accept everything that is actually benign, you just need to make it easy to write benign code that passes the check.
    - chriswarbo 11y ago
      Technically, Rice's theorem only applies to "non-trivial" questions, i.e. those which are true for some programs and false for others, which are properties of the function being computed. Hence we can work around the theorem, by either turning the questions we care about into trivial questions, or by turning questions of the function into questions about the implementation. For example, we might ask the question "Will program P fire the missiles?". If the answer is yes for some P and false for others, then we cannot answer it for arbitrary P. We can work around it by weakening the question to become trivial, e.g. "Is program P capable of firing missiles?". If the language allows missiles to be fired, then the answer is trivially yes for all P; if not then the answer is trivially no. Alternatively, we can change the question to one of implementation, e.g. "Does program P contain the <fire missiles> instruction?". Assuming that our programming language contains such an instruction, this is a non-trivial question. However, since it's a question about the implementation (does that instruction appear) rather than the function being computed (which may or may not fire missiles), Rice's theorem doesn't forbid us from answering it.
- logicrook 11y ago
  This is more from the perspective of the language designer, not from a "you get a binary, is it malware" one, in which case Turing-completeness basically has no importance. So for an example... Many exploits use stackoverflows to get the execution of arbitrary code. You can prove that in some bounded languages such things cannot happen, regardless of the inputs the program gets. Obviously you still rely on assumptions such as "the OS is not going to do random things with the memory", but that's outside of your power anyway.
- coldtea 11y ago
  >I sort of get what you are saying, that Turing completeness makes analysis more difficult, but I still don't see what it has to do with security. If analysis was easy you could prove (as in mathematically, e.g. with type theory and such) that the program could never get in certain insecure states. In fact, lots of highly secure environments (NASA etc), require just such proofs from certain programming modules in order to use them.
  - adrianN 11y ago
    Turing completeness of the language is only a problem if you don't want to reject safe programs. If you're fine with false positives you can just check (using a regex!) that no \write happens. Static analysis (not using regexes) is a thing for Turing complete languages and can prove non-trivial things.
- robert_tweed 11y ago
  A turing complete program could, by definition, generate any other turing complete program. In theory, you can statically analyse any program to prove that it doesn't contain malicious code (for some definition of malicious). But if a program is turing complete, you cannot predict all of its possible outputs and therefore, cannot rule out the possibility of a malicious output. The halting problem is what prevents you doing the analysis, not what introduces the possibility of maliciousness.
chriswarbo 11y ago
> if your language is not Turing-complete, you could lock things down so that no crazy stuff happens, and prove that there is no way to bypass the security --assuming this problem is decidable, which can be the case if the language is not Turin-complete, but is hopeless otherwise. It might be hopeless to try and "lock down" a Turing-complete language, but that's the wrong way to approach the problem. Rather than allowing undesired effects then trying to show they don't happen, simply avoid including them in the first place. For example, consider an implementation of Conway's Game of Life, which takes in a text file describing the initial pattern (program), keeps running it until some stopping criterion is met (say, when the cell at position (0, 0) in the text file first becomes live), and outputs either the final state of the grid, or an error message (parse error, out of memory, etc.). The Game of Life is Turing Complete[1], so it's undecidable in general whether a given text file will eventually produce a given pattern[2], including whether or not it will eventually trigger the stopping criterion. However, it's trivial to prove that our Game of Life implementation is secure against, say, shell execution attacks. How? We just need to prove that there are no patterns which cause shell execution. Since the Game of Life "language" has no concept of shell execution, our implementation doesn't need to expose anything which could allow it; it just needs to get and set booleans in an array, so this should be very straightforward to prove, even in a dangerous language like C. Just by verifying a single, known piece of code (our interpreter) we gain a security proof for all Game of Life programs. Of course the Game of Life is a simplistic example, but this idea has been around for a while in functional programming, where it's common to solve a problem by first embedding a DSL (domain-specific language) inside our main or "host" language, then coding the solution in that DSL. This lets us, for example, write a parser using a DSL specifically tailored for parsing, or describe a diagram in a DSL specially tailored for drawing diagrams, etc. We can prove all sorts of things about these DSLs, even if they're Turing Complete, by simply making them incapable of doing anything we don't want them to do. Since the "host" language (Lisp, Haskell, etc.) can already do potentially-dangerous things like accessing the filesystem, calling out to a shell, etc. there's no need to provide any of those features to the DSLs. For example, if we want to parse the contents of an arbitrary file `F` using an arbitrary parsing program `P`, we can write a small piece of code in the host language for reading the contents of `F` as a string, then passing this string and `P` as arguments to the parsing DSL interpreter. This way, neither the parsing DSL or its interpreter need any access to the filesystem, so it can be straightforward to prove that no filesystem operations (e.g. accessing unauthorised data) can take place, regardless of what `F` and `P` are. Likewise, if we want to render a diagram described by an arbitrary program `D` to an image file `I`, there's no need to provide filesystem access to the diagram DSL. Instead, we pass `D` to the diagram DSL interpreter and have it produce, say, an array of PNG data. The host language can then write this data to `I`, and again we can prove all kinds of properties like not overwriting a user's files, regardless of the program `D`. Another nice benefit of using restricted DSLs like this is the ability to intercept all effects which we do provide to the language. For example, just because we provide `read(path)` and `write(path, string)` primitive to our DSL, doesn't mean that such programs can access the filesystem. We might choose to have an interpreter which implements these by reading and writing files, but we can just as well write an interpreter which loads and stores strings in a hash table. This is useful for testing, debugging, tracing, etc. [1] http://rendell-attic.org/gol/utm/index.htm http://rendell-attic.org/gol/utm/index.htm [2] This only holds "in general"; there are particular patterns which are decidable, known as "Garden of Eden" patterns; these cannot exist after the first time step, so we just need to check whether they appear as-is in the initial program https://en.wikipedia.org/wiki/Garden_of_Eden_(cellular_automaton) https://en.wikipedia.org/wiki/Garden_of_Eden_(cellular_autom...

radarsat1 11y ago

Can you give an example of how the halting problem allows one to make it impossible/difficult to detect malicious code? I sort of get what you are saying, that Turing completeness makes analysis more difficult, but I still don't see what it has to do with security.

yk 11y ago
Well, if you can somehow inject arbitrary code, then you can inject an infinite loop. So a program will only halt on all inputs if you can not inject an infinite loop.
- radarsat1 11y ago
  Sure.. so how is an infinite loop a security vulnerability?
  - JadeNB 11y ago
    If you are performing data processing on user-supplied inputs (as online compilers do), then an infinite loop can amount to a DoS attack.
  - yk 11y ago
    The argument is the other way around, if a program halts on all inputs, then there is no possibility to inject arbitrary code. ( There may still be important security vulnerabilities, but there are some limits. Consider a debugger that executes the first 10 000 operations of a program, it would halt, but 10 000 operations is a lot of space to do something malicious.)
  - coldtea 11y ago
    Security doesn't end with "privilege escalation". "Killing" (DoS) a system is also an attack.
yaps8 11y ago
The halting problem makes it impossible to consistently answer the question "Will this instruction be executed ?" This is why you can't know if the code is malicious : you can't (always) infer meaningful properties about the code (Will it write something on the disk ?...).
- JadeNB 11y ago
  > The halting problem makes it impossible to consistently answer the question "Will this instruction be executed ?" In fact, Rice's theorem says that it's impossible more generally to answer any question about arbitrary code—so no work-arounds like "OK, I can't tell if a particular instruction is executed, but I can just test whether this program is 'safe'" (say, performs no I/O).
  - 9mit3t2m9h9a 11y ago
    And the reason why you cannot check that the program performs no I/O is because you cannot check if the I/O instructions are behind an infinite loop or an impossible condition or not. It is definitely easy to verify that a program has no references to I/O instructions. This will reject programs like «if(false) then write("Hello")», so it is not a violation of Rice theorem (functionally equivalent programs are not treated in the same way). But you don't need to accept everything that is actually benign, you just need to make it easy to write benign code that passes the check.
  - chriswarbo 11y ago
    Technically, Rice's theorem only applies to "non-trivial" questions, i.e. those which are true for some programs and false for others, which are properties of the function being computed. Hence we can work around the theorem, by either turning the questions we care about into trivial questions, or by turning questions of the function into questions about the implementation. For example, we might ask the question "Will program P fire the missiles?". If the answer is yes for some P and false for others, then we cannot answer it for arbitrary P. We can work around it by weakening the question to become trivial, e.g. "Is program P capable of firing missiles?". If the language allows missiles to be fired, then the answer is trivially yes for all P; if not then the answer is trivially no. Alternatively, we can change the question to one of implementation, e.g. "Does program P contain the <fire missiles> instruction?". Assuming that our programming language contains such an instruction, this is a non-trivial question. However, since it's a question about the implementation (does that instruction appear) rather than the function being computed (which may or may not fire missiles), Rice's theorem doesn't forbid us from answering it.
logicrook 11y ago
This is more from the perspective of the language designer, not from a "you get a binary, is it malware" one, in which case Turing-completeness basically has no importance. So for an example... Many exploits use stackoverflows to get the execution of arbitrary code. You can prove that in some bounded languages such things cannot happen, regardless of the inputs the program gets. Obviously you still rely on assumptions such as "the OS is not going to do random things with the memory", but that's outside of your power anyway.
coldtea 11y ago
>I sort of get what you are saying, that Turing completeness makes analysis more difficult, but I still don't see what it has to do with security. If analysis was easy you could prove (as in mathematically, e.g. with type theory and such) that the program could never get in certain insecure states. In fact, lots of highly secure environments (NASA etc), require just such proofs from certain programming modules in order to use them.
- adrianN 11y ago
  Turing completeness of the language is only a problem if you don't want to reject safe programs. If you're fine with false positives you can just check (using a regex!) that no \write happens. Static analysis (not using regexes) is a thing for Turing complete languages and can prove non-trivial things.
robert_tweed 11y ago
A turing complete program could, by definition, generate any other turing complete program. In theory, you can statically analyse any program to prove that it doesn't contain malicious code (for some definition of malicious). But if a program is turing complete, you cannot predict all of its possible outputs and therefore, cannot rule out the possibility of a malicious output. The halting problem is what prevents you doing the analysis, not what introduces the possibility of maliciousness.

chriswarbo 11y ago

> if your language is not Turing-complete, you could lock things down so that no crazy stuff happens, and prove that there is no way to bypass the security --assuming this problem is decidable, which can be the case if the language is not Turin-complete, but is hopeless otherwise. It might be hopeless to try and "lock down" a Turing-complete language, but that's the wrong way to approach the problem. Rather than allowing undesired effects then trying to show they don't happen, simply avoid including them in the first place. For example, consider an implementation of Conway's Game of Life, which takes in a text file describing the initial pattern (program), keeps running it until some stopping criterion is met (say, when the cell at position (0, 0) in the text file first becomes live), and outputs either the final state of the grid, or an error message (parse error, out of memory, etc.). The Game of Life is Turing Complete[1], so it's undecidable in general whether a given text file will eventually produce a given pattern[2], including whether or not it will eventually trigger the stopping criterion. However, it's trivial to prove that our Game of Life implementation is secure against, say, shell execution attacks. How? We just need to prove that there are no patterns which cause shell execution. Since the Game of Life "language" has no concept of shell execution, our implementation doesn't need to expose anything which could allow it; it just needs to get and set booleans in an array, so this should be very straightforward to prove, even in a dangerous language like C. Just by verifying a single, known piece of code (our interpreter) we gain a security proof for all Game of Life programs. Of course the Game of Life is a simplistic example, but this idea has been around for a while in functional programming, where it's common to solve a problem by first embedding a DSL (domain-specific language) inside our main or "host" language, then coding the solution in that DSL. This lets us, for example, write a parser using a DSL specifically tailored for parsing, or describe a diagram in a DSL specially tailored for drawing diagrams, etc. We can prove all sorts of things about these DSLs, even if they're Turing Complete, by simply making them incapable of doing anything we don't want them to do. Since the "host" language (Lisp, Haskell, etc.) can already do potentially-dangerous things like accessing the filesystem, calling out to a shell, etc. there's no need to provide any of those features to the DSLs. For example, if we want to parse the contents of an arbitrary file `F` using an arbitrary parsing program `P`, we can write a small piece of code in the host language for reading the contents of `F` as a string, then passing this string and `P` as arguments to the parsing DSL interpreter. This way, neither the parsing DSL or its interpreter need any access to the filesystem, so it can be straightforward to prove that no filesystem operations (e.g. accessing unauthorised data) can take place, regardless of what `F` and `P` are. Likewise, if we want to render a diagram described by an arbitrary program `D` to an image file `I`, there's no need to provide filesystem access to the diagram DSL. Instead, we pass `D` to the diagram DSL interpreter and have it produce, say, an array of PNG data. The host language can then write this data to `I`, and again we can prove all kinds of properties like not overwriting a user's files, regardless of the program `D`. Another nice benefit of using restricted DSLs like this is the ability to intercept all effects which we do provide to the language. For example, just because we provide `read(path)` and `write(path, string)` primitive to our DSL, doesn't mean that such programs can access the filesystem. We might choose to have an interpreter which implements these by reading and writing files, but we can just as well write an interpreter which loads and stores strings in a hash table. This is useful for testing, debugging, tracing, etc. [1] http://rendell-attic.org/gol/utm/index.htm http://rendell-attic.org/gol/utm/index.htm [2] This only holds "in general"; there are particular patterns which are decidable, known as "Garden of Eden" patterns; these cannot exist after the first time step, so we just need to check whether they appear as-is in the initial program https://en.wikipedia.org/wiki/Garden_of_Eden_(cellular_automaton) https://en.wikipedia.org/wiki/Garden_of_Eden_(cellular_autom...