On Mon, Apr 11, 2016 at 9:04 PM, Isaac Morland <ijmor...@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 _______________________________________________ Python-Dev mailing list Python-Dev@python.org https://mail.python.org/mailman/listinfo/python-dev Unsubscribe: https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com
