Jeremy Hylton : weblog : 2003-12-10

A Toy Bytecode Verifier

Wednesday, December 10, 2003, 11:52 p.m.

I tried to write a little bytecode verifier for RestrictedPython that guaranteed that dangerous opcodes -- like STORE_SUBSCR -- were guarded properly as the result of the compiler transformations and custom code generator in RestrictedPython. The simple opcodes like LOAD_ATTR and UNPACK_SEQUENCE are easy to handle; the rest was too big an effort for this evening.

To verify that an opcod like STORE_SUBSCR is called in a safe way, you have to verify that it's container argument is either a checked object or a dict literal created with BUILD_MAP. Since the dict key can be an arbitrary expression, you need to do abstract interpretation with a simple type system to guarantee that the operation is safe. I was trying to do this in about 30 minutes, and didn't have time to simulate the type and stack effects on all the Python opcodes (ha!).

The goal of this project is to provide a complete check of the correctness of the transformation system. We can specify the basic security policy with respect to the bytecode, and verify that the generated bytecode honors this policy. That's a nice check that everything is working, but probably too ambitious for the current task.