Patent ID: 8375443

Claim:
A computer-implemented method for ensuring that user code executes safely, comprising: loading, using a processor, user code and system method code defining a set of system methods in one or more system method libraries that are called by the user code, wherein the system method code has embedded annotations that provide information about safety properties of respective system methods with which the annotations are associated; dividing the set of system methods into safe system methods and unsafe system methods based on the annotations, wherein a safe method is a method that cannot violate safety properties regardless of the values of its parameters, and wherein an unsafe method is a method for which one or more parameter values exist that cause the method to violate safety properties, wherein the annotations associated with one or more unsafe system methods specify safety threats that the respective system methods can cause; executing the loaded user code when an offline audit of the system method code verifies that the annotations provide a valid code safety perimeter for the loaded user code, wherein a code safety perimeter establishes which system methods are visible to user code, a code safety perimeter is valid when only safe system methods are visible to user code, and unsafe system methods must be called via a safe system method rather than being directly visible to user code, wherein the set of system methods includes one or more safe system methods that are managed methods for one or more unsafe system methods, wherein the managed methods call the unsafe system methods while enforcing parameter restrictions specified by the annotations, and wherein the offline audit verifies as valid a code safety perimeter in which the managed methods are visible to user code and allow access to the unsafe system methods, but the unsafe system methods themselves are not visible to the user code; and preventing execution of the loaded user code when the offline audit of the system method code verifies that the annotations do not provide a valid code safety perimeter for the loaded user code.