234 lines
8.6 KiB
Plaintext
234 lines
8.6 KiB
Plaintext
PEP: 330
|
|
Title: Python Bytecode Verification
|
|
Version: $Revision$
|
|
Last-Modified: $Date$
|
|
Author: Michel Pelletier <michel@users.sourceforge.net>
|
|
Status: Rejected
|
|
Type: Standards Track
|
|
Content-Type: text/x-rst
|
|
Created: 17-Jun-2004
|
|
Python-Version: 2.6
|
|
Post-History:
|
|
|
|
|
|
Abstract
|
|
========
|
|
|
|
If Python Virtual Machine (PVM) bytecode is not "well-formed" it
|
|
is possible to crash or exploit the PVM by causing various errors
|
|
such as under/overflowing the value stack or reading/writing into
|
|
arbitrary areas of the PVM program space. Most of these kinds of
|
|
errors can be eliminated by verifying that PVM bytecode does not
|
|
violate a set of simple constraints before execution.
|
|
|
|
This PEP proposes a set of constraints on the format and structure
|
|
of Python Virtual Machine (PVM) bytecode and provides an
|
|
implementation in Python of this verification process.
|
|
|
|
|
|
Pronouncement
|
|
=============
|
|
|
|
Guido believes that a verification tool has some value. If
|
|
someone wants to add it to ``Tools/scripts``, no PEP is required.
|
|
|
|
Such a tool may have value for validating the output from
|
|
"bytecodehacks" or from direct edits of PYC files. As security
|
|
measure, its value is somewhat limited because perfectly valid
|
|
bytecode can still do horrible things. That situation could
|
|
change if the concept of restricted execution were to be
|
|
successfully resurrected.
|
|
|
|
|
|
Motivation
|
|
==========
|
|
|
|
The Python Virtual Machine executes Python programs that have been
|
|
compiled from the Python language into a bytecode representation.
|
|
The PVM assumes that any bytecode being executed is "well-formed"
|
|
with regard to a number implicit constraints. Some of these
|
|
constraints are checked at run-time, but most of them are not due
|
|
to the overhead they would create.
|
|
|
|
When running in debug mode the PVM does do several run-time checks
|
|
to ensure that any particular bytecode cannot violate these
|
|
constraints that, to a degree, prevent bytecode from crashing or
|
|
exploiting the interpreter. These checks add a measurable
|
|
overhead to the interpreter, and are typically turned off in
|
|
common use.
|
|
|
|
Bytecode that is not well-formed and executed by a PVM not running
|
|
in debug mode may create a variety of fatal and non-fatal errors.
|
|
Typically, ill-formed code will cause the PVM to seg-fault and
|
|
cause the OS to immediately and abruptly terminate the
|
|
interpreter.
|
|
|
|
Conceivably, ill-formed bytecode could exploit the interpreter and
|
|
allow Python bytecode to execute arbitrary C-level machine
|
|
instructions or to modify private, internal data structures in the
|
|
interpreter. If used cleverly this could subvert any form of
|
|
security policy an application may want to apply to its objects.
|
|
|
|
Practically, it would be difficult for a malicious user to
|
|
"inject" invalid bytecode into a PVM for the purposes of
|
|
exploitation, but not impossible. Buffer overflow and memory
|
|
overwrite attacks are commonly understood, particularly when the
|
|
exploit payload is transmitted unencrypted over a network or when
|
|
a file or network security permission weakness is used as a
|
|
foothold for further attacks.
|
|
|
|
Ideally, no bytecode should ever be allowed to read or write
|
|
underlying C-level data structures to subvert the operation of the
|
|
PVM, whether the bytecode was maliciously crafted or not. A
|
|
simple pre-execution verification step could ensure that bytecode
|
|
cannot over/underflow the value stack or access other sensitive
|
|
areas of PVM program space at run-time.
|
|
|
|
This PEP proposes several validation steps that should be taken on
|
|
Python bytecode before it is executed by the PVM so that it
|
|
compiles with static and structure constraints on its instructions
|
|
and their operands. These steps are simple and catch a large
|
|
class of invalid bytecode that can cause crashes. There is also
|
|
some possibility that some run-time checks can be eliminated up
|
|
front by a verification pass.
|
|
|
|
There is, of course, no way to verify that bytecode is "completely
|
|
safe", for every definition of complete and safe. Even with
|
|
bytecode verification, Python programs can and most likely in the
|
|
future will seg-fault for a variety of reasons and continue to
|
|
cause many different classes of run-time errors, fatal or not.
|
|
The verification step proposed here simply plugs an easy hole that
|
|
can cause a large class of fatal and subtle errors at the bytecode
|
|
level.
|
|
|
|
Currently, the Java Virtual Machine (JVM) verifies Java bytecode
|
|
in a way very similar to what is proposed here. The JVM
|
|
Specification version 2 [1]_, Sections 4.8 and 4.9 were therefore
|
|
used as a basis for some of the constraints explained below. Any
|
|
Python bytecode verification implementation at a minimum must
|
|
enforce these constraints, but may not be limited to them.
|
|
|
|
|
|
Static Constraints on Bytecode Instructions
|
|
===========================================
|
|
|
|
1. The bytecode string must not be empty. (``len(co_code) > 0``).
|
|
|
|
2. The bytecode string cannot exceed a maximum size
|
|
(``len(co_code) < sizeof(unsigned char) - 1``).
|
|
|
|
3. The first instruction in the bytecode string begins at index 0.
|
|
|
|
4. Only valid byte-codes with the correct number of operands can
|
|
be in the bytecode string.
|
|
|
|
|
|
Static Constraints on Bytecode Instruction Operands
|
|
===================================================
|
|
|
|
1. The target of a jump instruction must be within the code
|
|
boundaries and must fall on an instruction, never between an
|
|
instruction and its operands.
|
|
|
|
2. The operand of a ``LOAD_*`` instruction must be a valid index into
|
|
its corresponding data structure.
|
|
|
|
3. The operand of a ``STORE_*`` instruction must be a valid index
|
|
into its corresponding data structure.
|
|
|
|
|
|
Structural Constraints between Bytecode Instructions
|
|
====================================================
|
|
|
|
1. Each instruction must only be executed with the appropriate
|
|
number of arguments in the value stack, regardless of the
|
|
execution path that leads to its invocation.
|
|
|
|
2. If an instruction can be executed along several different
|
|
execution paths, the value stack must have the same depth prior
|
|
to the execution of the instruction, regardless of the path
|
|
taken.
|
|
|
|
3. At no point during execution can the value stack grow to a
|
|
depth greater than that implied by ``co_stacksize``.
|
|
|
|
4. Execution never falls off the bottom of ``co_code``.
|
|
|
|
|
|
Implementation
|
|
==============
|
|
|
|
This PEP is the working document for a Python bytecode
|
|
verification implementation written in Python. This
|
|
implementation is not used implicitly by the PVM before executing
|
|
any bytecode, but is to be used explicitly by users concerned
|
|
about possibly invalid bytecode with the following snippet::
|
|
|
|
import verify
|
|
verify.verify(object)
|
|
|
|
The ``verify`` module provides a ``verify`` function which accepts the
|
|
same kind of arguments as ``dis.dis``: classes, methods, functions,
|
|
or code objects. It verifies that the object's bytecode is
|
|
well-formed according to the specifications of this PEP.
|
|
|
|
If the code is well-formed the call to ``verify`` returns silently
|
|
without error. If an error is encountered, it throws a
|
|
``VerificationError`` whose argument indicates the cause of the
|
|
failure. It is up to the programmer whether or not to handle the
|
|
error in some way or execute the invalid code regardless.
|
|
|
|
Phillip Eby has proposed a pseudo-code algorithm for bytecode
|
|
stack depth verification used by the reference implementation.
|
|
|
|
|
|
Verification Issues
|
|
===================
|
|
|
|
This PEP describes only a small number of verifications. While
|
|
discussion and analysis will lead to many more, it is highly
|
|
possible that future verification may need to be done or custom,
|
|
project-specific verifications. For this reason, it might be
|
|
desirable to add a verification registration interface to the test
|
|
implementation to register future verifiers. The need for this is
|
|
minimal since custom verifiers can subclass and extend the current
|
|
implementation for added behavior.
|
|
|
|
|
|
Required Changes
|
|
================
|
|
|
|
Armin Rigo noted that several byte-codes will need modification in
|
|
order for their stack effect to be statically analyzed. These are
|
|
``END_FINALLY``, ``POP_BLOCK``, and ``MAKE_CLOSURE``. Armin and Guido have
|
|
already agreed on how to correct the instructions. Currently the
|
|
Python implementation punts on these instructions.
|
|
|
|
This PEP does not propose to add the verification step to the
|
|
interpreter, but only to provide the Python implementation in the
|
|
standard library for optional use. Whether or not this
|
|
verification procedure is translated into C, included with the PVM
|
|
or enforced in any way is left for future discussion.
|
|
|
|
|
|
References
|
|
==========
|
|
|
|
.. [1] The Java Virtual Machine Specification 2nd Edition
|
|
http://java.sun.com/docs/books/vmspec/2nd-edition/html/ClassFile.doc.html
|
|
|
|
|
|
Copyright
|
|
=========
|
|
|
|
This document has been placed in the public domain.
|
|
|
|
|
|
..
|
|
Local Variables:
|
|
mode: indented-text
|
|
indent-tabs-mode: nil
|
|
sentence-end-double-space: t
|
|
fill-column: 70
|
|
End:
|