Title: Proof Carrying Code and Lua

Abstract:
Formal methods of software verification are used to ensure the safety and reliability of computer programs. Based upon mathematical and logical foundations, formal methods can rigorously prove the functioning and correctness of code used in situations where reliability is a requirement.

Proof-carrying code is a formal method of proving the safety of machine language programs, and is especially suited to scenarios where the generator of code is distinct from the code consumer. Before loading and executing, code is verified to conform to a formal logical proof of safety and correctness. After this verification occurs, execution can proceed without expensive run-time verification conditions.

This presentation will discuss implementing a proof-carrying code system for the virtual machine instruction set of the Lua language. Details of the implementation, including trade-offs required by the Lua language, will also be presented.