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.
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.
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.
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 ?...).
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).
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.
You're quite right that my omission of 'non-trivial' makes the theorem as stated wrong; sorry!
I like your statement of the second work-around (elaborated below (https://news.ycombinator.com/item?id=11260034)), as (essentially) what type systems do, especially with the emphasis on why it must be over-conservative.
Although your statement of the first work-around is technically correct, I think that it is important to emphasise (as you clearly know, but others may not) how useless it is (on the program level): questions of this sort are necessarily about the language, not about the program.
On common architectures where code is data is code, this sounds hard to detect as the program could build a buffer of commands that end up firing the missile, without any obvious "fire the missile" sequence present in the binary? For example, the program could inflict a stack overflow on itself.
Absolutely, the work-arounds are just that; they don't answer the original question.
In the case of "Is program P capable of firing missiles?", this will be 'yes' for many programs which don't fire missiles, so it's an over-approximation of missile-firing.
In the case of "Does program P contain the <fire missiles> instruction?", this could, as you say, under-approximate missile firing.
If the language allows running data as code, then we can handle this in a conservative way, i.e. 'Could program P execute a <fire missiles> instruction?', which would be true if P contains '<fire missiles>', true if P contains 'eval' (since the evaluated code could fire the missiles), etc. and false otherwise. We can make our questions (AKA our type systems) arbitrarily clever, but they will only ever approximate the answers to questions forbidden by Rice's theorem. Usually it's best to make conservative approximations, i.e. turning "does XYZ happen?" into "could XYZ happen?", assuming that it could, and only answering 'no' if we can prove otherwise.
As far as cases like 'the program could inflict a stack overflow on itself', these would all be handled in our model of the language (equivalent to the list of conditions I wrote above which affected whether we answer true or false). Again, this should be conservative, so it's likely that for edge-cases like 'inflicting a stack overflow on itself', there might not be much we can say about the program's behaviour; in which case we'd get a lot of 'yes' answers to our 'could XYZ happen?' questions, simply because we can't rule those things out.
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.
"Killing" (DoS) a system is also an attack.
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.
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
[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_autom...
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.