Efficient, Verifiable Binary Sandboxing for a CISC Architecture
Executing untrusted code while preserving security requiresenforcement of memory and control-flow safety policies:untrusted code must be prevented from modifying memory orexecuting code except as explicitly allowed. Software-basedfault isolation (SFI) or \"sandboxing\" enforces thosepolic...
| Κύριοι συγγραφείς: | , |
|---|---|
| Άλλοι συγγραφείς: | |
| Γλώσσα: | en_US |
| Έκδοση: |
2005
|
| Διαθέσιμο Online: | http://hdl.handle.net/1721.1/30542 |
| _version_ | 1826204504425496576 |
|---|---|
| author | McCamant, Stephen Morrisett, Greg |
| author2 | Program Analysis |
| author_facet | Program Analysis McCamant, Stephen Morrisett, Greg |
| author_sort | McCamant, Stephen |
| collection | MIT |
| description | Executing untrusted code while preserving security requiresenforcement of memory and control-flow safety policies:untrusted code must be prevented from modifying memory orexecuting code except as explicitly allowed. Software-basedfault isolation (SFI) or \"sandboxing\" enforces thosepolicies by rewriting the untrusted code at the level ofindividual instructions. However, the original sandboxingtechnique of Wahbe et al. is applicable only to RISCarchitectures, and other previous work is either insecure,or has been not described in enough detail to giveconfidence in its security properties. We present a noveltechnique that allows sandboxing to be easily applied to aCISC architecture like the IA-32. The technique can beverified to have been applied at load time, so that neitherthe rewriting tool nor the compiler needs to be trusted. Wedescribe a prototype implementation which provides a robustsecurity guarantee, is scalable to programs of any size, andhas low runtime overheads. Further, we give amachine-checked proof that any program approved by theverification algorithm is guaranteed to respect the desiredsafety property. |
| first_indexed | 2024-09-23T12:56:40Z |
| id | mit-1721.1/30542 |
| institution | Massachusetts Institute of Technology |
| language | en_US |
| last_indexed | 2024-09-23T12:56:40Z |
| publishDate | 2005 |
| record_format | dspace |
| spelling | mit-1721.1/305422019-04-11T06:23:27Z Efficient, Verifiable Binary Sandboxing for a CISC Architecture McCamant, Stephen Morrisett, Greg Program Analysis Executing untrusted code while preserving security requiresenforcement of memory and control-flow safety policies:untrusted code must be prevented from modifying memory orexecuting code except as explicitly allowed. Software-basedfault isolation (SFI) or \"sandboxing\" enforces thosepolicies by rewriting the untrusted code at the level ofindividual instructions. However, the original sandboxingtechnique of Wahbe et al. is applicable only to RISCarchitectures, and other previous work is either insecure,or has been not described in enough detail to giveconfidence in its security properties. We present a noveltechnique that allows sandboxing to be easily applied to aCISC architecture like the IA-32. The technique can beverified to have been applied at load time, so that neitherthe rewriting tool nor the compiler needs to be trusted. Wedescribe a prototype implementation which provides a robustsecurity guarantee, is scalable to programs of any size, andhas low runtime overheads. Further, we give amachine-checked proof that any program approved by theverification algorithm is guaranteed to respect the desiredsafety property. 2005-12-22T02:28:49Z 2005-12-22T02:28:49Z 2005-05-02 MIT-CSAIL-TR-2005-030 MIT-LCS-TR-988 http://hdl.handle.net/1721.1/30542 en_US Massachusetts Institute of Technology Computer Science and Artificial Intelligence Laboratory 17 p. 29512899 bytes 1053603 bytes application/postscript application/pdf application/postscript application/pdf |
| spellingShingle | McCamant, Stephen Morrisett, Greg Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title | Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title_full | Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title_fullStr | Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title_full_unstemmed | Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title_short | Efficient, Verifiable Binary Sandboxing for a CISC Architecture |
| title_sort | efficient verifiable binary sandboxing for a cisc architecture |
| url | http://hdl.handle.net/1721.1/30542 |
| work_keys_str_mv | AT mccamantstephen efficientverifiablebinarysandboxingforaciscarchitecture AT morrisettgreg efficientverifiablebinarysandboxingforaciscarchitecture |