4 ms·

> 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 f

> 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 5y 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 5y 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 5y 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 5y 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 5y 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 5y 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."

sterlind 5y 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 5y 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 5y 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 5y 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 5y 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 5y 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."