[Python-Dev] Challenge: Please break this! (a.k.a restricted mode revisited) (original) (raw)

Chris Angelico rosuav at gmail.com
Mon Apr 11 12:01:33 EDT 2016

On Mon, Apr 11, 2016 at 9:04 PM, Isaac Morland <ijmorlan at uwaterloo.ca> wrote:

But I would not use for security purposes a Python sandbox that was not formally verified to be correct and unbreakable. Of course in order for this to be possible, there first has to be a formal semantics for Python. Has anybody made a formal semantics for Python? If not, then this project is missing a pretty important pre-requisite.

Formal semantics for the language? Yes; most of docs.python.org is about the language, independently of any particular implementation. (There are odd notes here and there about "CPython implementation detail" and such, and there are some entire modules that are specifically stated as being implementation-specific, but they're a tiny proportion.) You can also read through the PEPs, which (again, for the most part) deal with language-level concerns ahead of implementation details.

However, even with that information, it's virtually impossible to formally verify that the sandbox is unbreakable. A Python-in-Python sandbox is almost guaranteed to leak information across the boundary, and when information is leaked, it's extremely hard to prove that privilege escalation is impossible.

ChrisA

More information about the Python-Dev mailing list