Safe Kernel Extensions Without Run-Time Checking Export

@inproceedings{citeulike:251671, abstract = {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 first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal proof that the code obeys the safety policy. The kernel can easily validate the...}, address = {Berkeley, CA, USA}, author = {Necula, George C. and Lee, Peter}, booktitle = {2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28--31, 1996. Seattle, {WA}}, citeulike-article-id = {251671}, citeulike-linkout-0 = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.3010}, editor = {Useni, X.}, keywords = {kernel, operating-system, proof-carrying-code}, pages = {229--243}, posted-at = {2009-07-10 02:34:19}, priority = {2}, publisher = {USENIX}, title = {Safe Kernel Extensions Without Run-Time Checking}, url = {http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.3010}, year = {1996} }

TY - CONF ID - citeulike:251671 L3 - citeulike-article-id:251671 N2 - 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 first defines a safety policy and makes it public. Then, using this policy, an application can provide binaries in a special form called proof-carrying code, or simply PCC. Each PCC binary contains, in addition to the native code, a formal proof that the code obeys the safety policy. The kernel can easily validate the... AD - Berkeley, CA, USA EP - 243 TI - Safe Kernel Extensions Without Run-Time Checking PB - USENIX T2 - 2nd Symposium on Operating Systems Design and Implementation (OSDI '96), October 28--31, 1996. Seattle, {WA} SP - 229 KW - kernel KW - operating-system KW - proof-carrying-code AU - Necula, George AU - Lee, Peter A2 - Useni, X PY - 1996/// UR - http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.40.3010 ER -