> That's because Latex is turing complete and that means...
The article is of course interesting, but it's really annoying to read claims that Turing completeness has anything to do with security. The danger comes from interaction with the external environment, not whether or not the language is Turing complete. If HTML had a "\write" equivalent, it would be just as dangerous. Conversely, the script,
Doesn't require a loop or anything indicating a Turing complete language. That said the Turing complete aspects of Latex can be very useful, for e.g. using it to calculate results during compilation. But it's the \write etc that make it dangerous, not \loop.
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.
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.
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.)
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 ?...).
> 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).
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.
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.
> 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)
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.
> 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
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.
> 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.
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.
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.
>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.
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.
> 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 an...
Though a longtime TeXer, I've never used the output facilities very much, so it's probably my fault; but I can't understand what this does (hence what it illustrates), and some things seem like typos. For example, shouldn't `\imm\diate`, `\wwrite`, and `\iput` be `\immediate`, `\write`, and `\input`? (I don't know about `\inp`.) What does this do?
The abbreviations are defined with the `\def` in the same code snippet. So that aren't typos, but a way to build latex commands like `\immediate` by breaking it up in multiple parts.
It should be noted that shell escape is disabled by default in standard installations and the -shell-escape flag must be explicitly passed during compilation to enable it.
So if someone is knowledgeable enough to add this flag I would assume that they know what they are doing, such as the guys cited in the article who create an isolated Docker container for each compilation cycle [note: very nice use of Docker!].
With the caveat, of course, that when it comes to security you can't just say "Docker and done". Docker is one layer of defense but it's not completely vetted and depending on it to fix all your security problems is a terrible practice to get into.
TeX files are a common method of collaboration for computer science professionals. It is widely assumed by users that LaTeX files are safe; that is, that no significant harm can come of running LaTeX on an arbitrary computer. Unfortunately, this is not the case: In this article we describe how to exploit LaTeX to build a virus that spreads between documents on the MiKTeX distribution on
Windows XP as well as how to use malicious documents to steal data from web-based LaTeX previewer services.
Edit: It seems at least TeXlive has configuration options to disallow access to files outside the current directory: http://tex.stackexchange.com/a/116927
People who cultivate a level of attention to detail that is seen as pedantic by many, but that is utterly essential for creating high quality software.
Maybe we can get some of those people to work on LaTeX.
For example, why should the commands for upright Greek letters be different for different fonts? \upalpha for one font, \alphaup for another, and \otheralpha for another -- it's a damn mess.
Perhaps someone who's cultivated a level of attention to detail could spend some time fixing this kind of buggy crap, instead of spending time telling people how to properly capitalize LaTeX.
You don't need something to be turing complete to exploit it and something being turing-complete doesn't mean you can exploit it (except DoS, if the process isn't killed automatically after a while).
39 comments
[ 2.9 ms ] story [ 79.6 ms ] threadThe article is of course interesting, but it's really annoying to read claims that Turing completeness has anything to do with security. The danger comes from interaction with the external environment, not whether or not the language is Turing complete. If HTML had a "\write" equivalent, it would be just as dangerous. Conversely, the script,
Doesn't require a loop or anything indicating a Turing complete language. That said the Turing complete aspects of Latex can be very useful, for e.g. using it to calculate results during compilation. But it's the \write etc that make it dangerous, not \loop.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.
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.
"Killing" (DoS) a system is also an attack.
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).
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.
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.
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.
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.
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.
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 an...
> \openout\outfile=cmd.tex
> \write\outfile{\imm\diate\wwrite\args}
> \write\outfile{\inp\iput\cmd}
> \closeout\outfile
Though a longtime TeXer, I've never used the output facilities very much, so it's probably my fault; but I can't understand what this does (hence what it illustrates), and some things seem like typos. For example, shouldn't `\imm\diate`, `\wwrite`, and `\iput` be `\immediate`, `\write`, and `\input`? (I don't know about `\inp`.) What does this do?
So if someone is knowledgeable enough to add this flag I would assume that they know what they are doing, such as the guys cited in the article who create an isolated Docker container for each compilation cycle [note: very nice use of Docker!].
https://news.ycombinator.com/item?id=7909622 (Docker container breakout?)
http://pages.physics.cornell.edu/~shicks/icfp08/proof.png
http://pages.physics.cornell.edu/~shicks/icfp08/proof.pdf
Also, from 2011: https://cseweb.ucsd.edu/~hovav/dist/tex-login.pdf
TeX files are a common method of collaboration for computer science professionals. It is widely assumed by users that LaTeX files are safe; that is, that no significant harm can come of running LaTeX on an arbitrary computer. Unfortunately, this is not the case: In this article we describe how to exploit LaTeX to build a virus that spreads between documents on the MiKTeX distribution on
Windows XP as well as how to use malicious documents to steal data from web-based LaTeX previewer services.
Edit: It seems at least TeXlive has configuration options to disallow access to files outside the current directory: http://tex.stackexchange.com/a/116927
Who cares, really?
I'd say its only essential for being no fun at parties.
For example, why should the commands for upright Greek letters be different for different fonts? \upalpha for one font, \alphaup for another, and \otheralpha for another -- it's a damn mess.
Perhaps someone who's cultivated a level of attention to detail could spend some time fixing this kind of buggy crap, instead of spending time telling people how to properly capitalize LaTeX.
You don't need something to be turing complete to exploit it and something being turing-complete doesn't mean you can exploit it (except DoS, if the process isn't killed automatically after a while).