4 ms·

This is oddly important. From the conclusion: > While this vulnerability has no real-world implications, we discuss whether it indicates an intrinsic propensit

This is oddly important. From the conclusion: > While this vulnerability has no real-world implications, we discuss whether it indicates an intrinsic propensityfor arbitrary code execution vulnerabilities in computers ingeneral. As a joke in the 90's I looked into writing malware for Napoleonic semaphore signalling networks (Chappe semaphore), with the idea that if it were possible, then nothing could be secure. We have some general ideas that nothing is secure, and that security is a relative quality and perception, but I don't know that we've been able to formalize it into a conjecture. (Other than Hofstadter's music to break phonographs by.) Maybe I'm missing a big obvious one, but there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity without first running it. Or maybe that there is a set of convolutions in a set of instructions whereafter the information it contains spirals off into chaos like the logistic equation and you can't formally predict how a program behaves based on its initial state. There's something about security problems that exist on the edge of computability and it seems like a perspective we could draw generalities from anyway.

Y_Y 6y ago
> "You know they'll never really die while the Trunk is alive [...] It lives while the code is shifted, and they live with it, always Going Home." - Moist von Lipwig, Going Postal, Chapter 13 This is a bit like the clacks network (inspired by semaphore) in the Discworld, and how you can spam it with everlasting messages, to memorialise the dead, or just gunk up the system.
umanwizard 6y ago
> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity without first running it. Rice’s theorem is a formal statement capturing what I think you mean here.
- sterlind 6y ago
  how does this apply to symbolic execution of programs? do you think it's possible to exploit a proof verifier through a maliciously-crafted set of lemmas?
  - maweki 6y ago
    Either your decision/deduction procedure terminates on all inputs. Then the property you're going after is trivial. Or it doesn't and then the property you're going after is generally undecidable. If you can symbolically evaluate a program and this always works for all input programs, your input programs are already restricted in that they are not computationally complete.
    - chriswarbo 6y ago
      Going a bit further, this could absolutely be used for a denial-of-service attack; but would otherwise be 'sandboxed', similar to how exploits for a Universal Turing machine are still limited to reading/writing the machine's tape. They can't, for example, hijack an SSH session or whatever (unless there are serious vulnerabilities in the prover/turing-machine implementation)
- motohagiography 6y ago
  https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem Thank you, that's the kind of example I was thinking must exist. It implies there is a program for each system that is undecidable, and then the question becomes how many of those programs transfer control so that the program rewrites itself. Maybe we don't need to do this in security, but sometimes it feels like the whole field is predicated on denying some foundational truth about complexity.
  - michaelt 6y ago
    Isn't the statement that "there exists a program for each system such that arbitrary code execution is possible" a tautology? Aren't you basically saying "Executing arbitrary code can allow executing arbitrary code"?
    - motohagiography 6y ago
      To a point, as there's no difference between authorized and unauthorized code, except there is, but there isn't.:) Maybe more like wondering what the consequences are if all code is arbitrary, particularly for higher order abstractions like security and economics. Security has always been a hall of mirrors, and a principle like this could be a fast heuristic for deciding how much risk you want to take. In all the security design work I've done, it was based on, "we've essentially made an attack cost greater than X, where X is close to the value of what they're protecting."
AndrewOMartin 6y ago
Forgive me if I'm wrong, but this video might suggest you were beaten to it by about 160 years! https://www.youtube.com/watch?v=cPeVsniB7b0 https://www.youtube.com/watch?v=cPeVsniB7b0
- motohagiography 6y ago
  So edifying! Deserves its own post really. They encoded data in a covert channel using backspaces, which is super interesting. The next level was looking for a way to change the contents of a message and potentially a code book update.
chriswarbo 6y ago
> Maybe I'm missing a big obvious one, but there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity without first running it. Yep, this is Rice's Theorem. If we have a particular program P which outputs a certain value, there is an infinite set of programs of the form 'C; P;' which first run some arbitrary code 'C' and then run P. The Halting Problem is undecidable, so we can't always tell whether code 'C' will halt or not; and hence whether we'll move on to executing P or not. More generally, Rice's Theorem applies to any non-trivial property of the input/output function implemented by a program. A non-trivial property means that at least one program has that property and at least one program doesn't. Being a property of the 'input/output function implemented by a program' avoids implementation details like 'runs for at least 10 steps'. The Halting Problem is semi-decidable: if we just run the given program until it halts then return 'HALTS', we will always return the correct answer when given a program which halts. This doesn't completely solve the Halting Problem, since we will not return 'NON-HALTING' when given a non-halting program (we will just run forever). Wolfram calls this "computational irreducibility": that the only way to predict the behaviour of a Turing-complete system is to simulate it; or, equivalently, any formula that tells us what will happen on the Nth step will, necessarily, involve calculating what happens on the (N-1)th step, the (N-2)th step, and so on back to the first step.
- wcarss 6y ago
  "O Great Univac, why did you ever create the universe?" "Someone asked if it would ever end."
spiritplumber 6y ago
GNU Terry Pratchett
chriswarbo 6y ago
> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity Just to focus on this idea of 'a certain complexity', you may like Chaitin's Incompleteness Theorem: https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin's_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin'... which defines the "algorithmic information content" of a symbolic system (whether that's a programming language or a mathematical logic; which are actually the same thing via the Curry-Howard correspondence!) The theorem is a bit technical, but basically involves a program which enumerates all strings of symbols from a chosen alphabet (pretty easy: just a `while` loop that tries longer and longer string lengths, and a `for` loop which goes through the alphabet over and over to output every combination of that many symbols). We use this to define a program which enumerates all proofs of some chosen formal logic (these are just strings of symbols which obey all of that logic's rules, so we just filter the output of the above program). We use this to define a program which enumerates proofs of theorems of the form "all programs which output string s contain at least N instructions" (this is just a pattern-match against the end of the proof). N is a parameter, whilst s can be any string (different proofs can have different strings s). We use this to define a final program, which we'll call P. Running P with a parameter, like P(N), will run the above enumeration for that value of N, and halt once a single proof has been found. Just before halting, P will output whichever string s appears in the proof it found. Now is the interesting part: we count up all of the instructions used to define all of the above programs. Let's call this U (as per the Wikipedia link above). We'll define another number N0 where N0 > U + the number of instructions required to define N0 in a program; in other words, N0 is more than the number of instructions needed to define 'P(N0)'. (Keep in mind that we can generate very large numbers using programs with only a few instructions, so it's easy enough to find a a suitable value of N0). Finally, consider what happens if we run the program P(N0): If P(N0) halts, it will output some particular string s. That string is taken from a proof of the theorem "all programs which output string s contain at least N0 instructions". We know that program P(N0) contains fewer than N0 instructions, which would contradict such a theorem. The only way to avoid this contradiction (other than using an inconsistent logic) is if P(N0) never halts. If P(N0) never halts, that means it will keep enumerating proofs forever without ever finding one for any theorem of the form "all programs which output string s contain at least N0 instructions"; for any string s. This latter result is consistent, but shows that our chosen system of logic (whatever it is), must be severely limited. In particular, we know it is unable to prove statements of the form "all programs which output string s contain at least N instructions" where N >= N0 (in fact, there's a lower bound on N0 based on 'compressing' the above programs into the fewest number of instructions; although finding that lower bound is uncomputable due to the halting problem!). At first glance this doesn't look very important, but consider the pigeonhole principle: there are only a finite number of programs with fewer than N0 instructions; hence there are only a finite number of strings 's' which can provably be generated with fewer than N0 instructions. Almost all strings 's' require more than N0 instructions to generate. Now consider programs of the form 'enumerate all proofs until we find one for statement T, then output T and halt'. If such a program contains more than N0 instructions, then our chosen logic is unable to prove whether this program will halt or not. We can prove that whether or not this program halts is equivalent to whether or not T is provable, and hence the only way for this halting/looping question to be unprovable is for the statement T to be unprovable. Hence almost all statements are unprovable by our given system of logic, regardless of which logic we choose! Chaitin takes this further, to define a "halting probability", and essentially shows that all mathematical 'knowledge' can be distilled down to set of which bits, which tell us whether certain programs halt or not.

Y_Y 6y ago

> "You know they'll never really die while the Trunk is alive [...] It lives while the code is shifted, and they live with it, always Going Home." - Moist von Lipwig, Going Postal, Chapter 13 This is a bit like the clacks network (inspired by semaphore) in the Discworld, and how you can spam it with everlasting messages, to memorialise the dead, or just gunk up the system.

umanwizard 6y ago

> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity without first running it. Rice’s theorem is a formal statement capturing what I think you mean here.

sterlind 6y ago
how does this apply to symbolic execution of programs? do you think it's possible to exploit a proof verifier through a maliciously-crafted set of lemmas?
- maweki 6y ago
  Either your decision/deduction procedure terminates on all inputs. Then the property you're going after is trivial. Or it doesn't and then the property you're going after is generally undecidable. If you can symbolically evaluate a program and this always works for all input programs, your input programs are already restricted in that they are not computationally complete.
  - chriswarbo 6y ago
    Going a bit further, this could absolutely be used for a denial-of-service attack; but would otherwise be 'sandboxed', similar to how exploits for a Universal Turing machine are still limited to reading/writing the machine's tape. They can't, for example, hijack an SSH session or whatever (unless there are serious vulnerabilities in the prover/turing-machine implementation)
motohagiography 6y ago
https://en.wikipedia.org/wiki/Rice%27s_theorem https://en.wikipedia.org/wiki/Rice%27s_theorem Thank you, that's the kind of example I was thinking must exist. It implies there is a program for each system that is undecidable, and then the question becomes how many of those programs transfer control so that the program rewrites itself. Maybe we don't need to do this in security, but sometimes it feels like the whole field is predicated on denying some foundational truth about complexity.
- michaelt 6y ago
  Isn't the statement that "there exists a program for each system such that arbitrary code execution is possible" a tautology? Aren't you basically saying "Executing arbitrary code can allow executing arbitrary code"?
  - motohagiography 6y ago
    To a point, as there's no difference between authorized and unauthorized code, except there is, but there isn't.:) Maybe more like wondering what the consequences are if all code is arbitrary, particularly for higher order abstractions like security and economics. Security has always been a hall of mirrors, and a principle like this could be a fast heuristic for deciding how much risk you want to take. In all the security design work I've done, it was based on, "we've essentially made an attack cost greater than X, where X is close to the value of what they're protecting."

AndrewOMartin 6y ago

Forgive me if I'm wrong, but this video might suggest you were beaten to it by about 160 years! https://www.youtube.com/watch?v=cPeVsniB7b0 https://www.youtube.com/watch?v=cPeVsniB7b0

motohagiography 6y ago
So edifying! Deserves its own post really. They encoded data in a covert channel using backspaces, which is super interesting. The next level was looking for a way to change the contents of a message and potentially a code book update.

chriswarbo 6y ago

> Maybe I'm missing a big obvious one, but there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity without first running it. Yep, this is Rice's Theorem. If we have a particular program P which outputs a certain value, there is an infinite set of programs of the form 'C; P;' which first run some arbitrary code 'C' and then run P. The Halting Problem is undecidable, so we can't always tell whether code 'C' will halt or not; and hence whether we'll move on to executing P or not. More generally, Rice's Theorem applies to any non-trivial property of the input/output function implemented by a program. A non-trivial property means that at least one program has that property and at least one program doesn't. Being a property of the 'input/output function implemented by a program' avoids implementation details like 'runs for at least 10 steps'. The Halting Problem is semi-decidable: if we just run the given program until it halts then return 'HALTS', we will always return the correct answer when given a program which halts. This doesn't completely solve the Halting Problem, since we will not return 'NON-HALTING' when given a non-halting program (we will just run forever). Wolfram calls this "computational irreducibility": that the only way to predict the behaviour of a Turing-complete system is to simulate it; or, equivalently, any formula that tells us what will happen on the Nth step will, necessarily, involve calculating what happens on the (N-1)th step, the (N-2)th step, and so on back to the first step.

wcarss 6y ago
"O Great Univac, why did you ever create the universe?" "Someone asked if it would ever end."

spiritplumber 6y ago

GNU Terry Pratchett

chriswarbo 6y ago

> there's something about programmable systems that they are necessarily unable to infer or deduce the output of a program beyond a certain complexity Just to focus on this idea of 'a certain complexity', you may like Chaitin's Incompleteness Theorem: https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin's_incompleteness_theorem https://en.wikipedia.org/wiki/Kolmogorov_complexity#Chaitin'... which defines the "algorithmic information content" of a symbolic system (whether that's a programming language or a mathematical logic; which are actually the same thing via the Curry-Howard correspondence!) The theorem is a bit technical, but basically involves a program which enumerates all strings of symbols from a chosen alphabet (pretty easy: just a `while` loop that tries longer and longer string lengths, and a `for` loop which goes through the alphabet over and over to output every combination of that many symbols). We use this to define a program which enumerates all proofs of some chosen formal logic (these are just strings of symbols which obey all of that logic's rules, so we just filter the output of the above program). We use this to define a program which enumerates proofs of theorems of the form "all programs which output string s contain at least N instructions" (this is just a pattern-match against the end of the proof). N is a parameter, whilst s can be any string (different proofs can have different strings s). We use this to define a final program, which we'll call P. Running P with a parameter, like P(N), will run the above enumeration for that value of N, and halt once a single proof has been found. Just before halting, P will output whichever string s appears in the proof it found. Now is the interesting part: we count up all of the instructions used to define all of the above programs. Let's call this U (as per the Wikipedia link above). We'll define another number N0 where N0 > U + the number of instructions required to define N0 in a program; in other words, N0 is more than the number of instructions needed to define 'P(N0)'. (Keep in mind that we can generate very large numbers using programs with only a few instructions, so it's easy enough to find a a suitable value of N0). Finally, consider what happens if we run the program P(N0): If P(N0) halts, it will output some particular string s. That string is taken from a proof of the theorem "all programs which output string s contain at least N0 instructions". We know that program P(N0) contains fewer than N0 instructions, which would contradict such a theorem. The only way to avoid this contradiction (other than using an inconsistent logic) is if P(N0) never halts. If P(N0) never halts, that means it will keep enumerating proofs forever without ever finding one for any theorem of the form "all programs which output string s contain at least N0 instructions"; for any string s. This latter result is consistent, but shows that our chosen system of logic (whatever it is), must be severely limited. In particular, we know it is unable to prove statements of the form "all programs which output string s contain at least N instructions" where N >= N0 (in fact, there's a lower bound on N0 based on 'compressing' the above programs into the fewest number of instructions; although finding that lower bound is uncomputable due to the halting problem!). At first glance this doesn't look very important, but consider the pigeonhole principle: there are only a finite number of programs with fewer than N0 instructions; hence there are only a finite number of strings 's' which can provably be generated with fewer than N0 instructions. Almost all strings 's' require more than N0 instructions to generate. Now consider programs of the form 'enumerate all proofs until we find one for statement T, then output T and halt'. If such a program contains more than N0 instructions, then our chosen logic is unable to prove whether this program will halt or not. We can prove that whether or not this program halts is equivalent to whether or not T is provable, and hence the only way for this halting/looping question to be unprovable is for the statement T to be unprovable. Hence almost all statements are unprovable by our given system of logic, regardless of which logic we choose! Chaitin takes this further, to define a "halting probability", and essentially shows that all mathematical 'knowledge' can be distilled down to set of which bits, which tell us whether certain programs halt or not.