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

[Chris Angelico]

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