Contents

• Abstract
• Pronouncement
• Motivation
• Static Constraints on Bytecode Instructions
• Static Constraints on Bytecode Instruction Operands
• Structural Constraints between Bytecode Instructions
• Implementation
• Verification Issues
• Required Changes
• References
• Copyright

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.