Sciweavers

OSDI
1996
ACM
14 years 2 months ago
Safe Kernel Extensions Without Run-Time Checking
This paper describes a mechanism by which an operating system kernel can determine with certainty that it is safe to execute a binary supplied by an untrusted source. The kernel r...
George C. Necula, Peter Lee
SCS
2001
14 years 2 months ago
Improved Acquisition Processes for Safety-Critical Systems in the Australian Department of Defence
This paper describes recently developed policy and procedures for safety management during system acquisition within the Australian government's Defence Materiel Organisation...
Peter A. Lindsay
CAISE
2006
Springer
14 years 4 months ago
Structuring Safety Policy Decomposition
Abstract. Safety policy is a collection of rules that govern the behaviour of entities such that they do not cause accidents. It has been suggested that policies in general can be ...
Martin Hall-May, Tim Kelly
FM
2003
Springer
108views Formal Methods» more  FM 2003»
14 years 5 months ago
Correctness of Source-Level Safety Policies
Abstract. Program certification techniques formally show that programs satisfy certain safety policies. They rely on the correctness of the safety policy which has to be establish...
Ewen Denney, Bernd Fischer 0002
IFIP
2004
Springer
14 years 6 months ago
Prototyping Proof Carrying Code
Abstract We introduce a generic framework for proof carrying code, developed and mechanically verified in Isabelle/HOL. The framework defines and proves sound a verification con...
Martin Wildmoser, Tobias Nipkow, Gerwin Klein, Seb...
ESOP
2005
Springer
14 years 6 months ago
Asserting Bytecode Safety
Abstract. We instantiate an Isabelle/HOL framework for proof carrying code to Jinja bytecode, a downsized variant of Java bytecode featuring objects, inheritance, method calls and ...
Martin Wildmoser, Tobias Nipkow
CADE
2002
Springer
15 years 29 days ago
A Gradual Approach to a More Trustworthy, Yet Scalable, Proof-Carrying Code
Abstract. Proof-carrying code (PCC) allows a code producer to associate to a program a machine-checkable proof of its safety. In the original approach to PCC, the safety policy inc...
Robert R. Schneck, George C. Necula