- Home
- Search Results
- Page 1 of 1
Search for: All records
-
Total Resources3
- Resource Type
-
03000000000
- More
- Availability
-
12
- Author / Contributor
- Filter by Author / Creator
-
-
Brown, Fraser (3)
-
Stefan, Deian (3)
-
Thien, David (3)
-
Jhala, Ranjit (2)
-
Renner, John (2)
-
Shacham, Hovav (2)
-
Sharma, Abhishek (2)
-
Smith, Naomi (2)
-
Alhessi, Yousef (1)
-
Johnson, Evan (1)
-
Lerner, Sorin (1)
-
McMullen, Tyler (1)
-
Narayan, Shravan (1)
-
Savage, Stefan (1)
-
#Tyler Phillips, Kenneth E. (0)
-
#Willis, Ciara (0)
-
& Abreu-Ramos, E. D. (0)
-
& Abramson, C. I. (0)
-
& Abreu-Ramos, E. D. (0)
-
& Adams, S.G. (0)
-
- Filter by Editor
-
-
Arpaci-Dusseau, Andrea (1)
-
Keeton, Kimberly (1)
-
null (1)
-
& Spizer, S. M. (0)
-
& . Spizer, S. (0)
-
& Ahn, J. (0)
-
& Bateiha, S. (0)
-
& Bosch, N. (0)
-
& Brennan K. (0)
-
& Brennan, K. (0)
-
& Chen, B. (0)
-
& Chen, Bodong (0)
-
& Drown, S. (0)
-
& Ferretti, F. (0)
-
& Higgins, A. (0)
-
& J. Peters (0)
-
& Kali, Y. (0)
-
& Ruiz-Arias, P.M. (0)
-
& S. Spitzer (0)
-
& Sahin. I. (0)
-
-
Have feedback or suggestions for a way to improve these results?
!
Note: When clicking on a Digital Object Identifier (DOI) number, you will be taken to an external site maintained by the publisher.
Some full text articles may not yet be available without a charge during the embargo (administrative interval).
What is a DOI Number?
Some links on this page may take you to non-federal websites. Their policies may differ from this site.
-
Arpaci-Dusseau, Andrea ; Keeton, Kimberly (Ed.)Just-in-time (JIT) compilers make JavaScript run efficiently by replacing slow JavaScript interpreter code with fast machine code. However, this efficiency comes at a cost: bugs in JIT compilers can completely subvert all language-based (memory) safety guarantees, and thereby introduce catastrophic exploitable vulnerabilities. We present Icarus: a new framework for implementing JIT compilers that are automatically, formally verified to be safe, and which can then be converted to C++ that can be linked into browser runtimes. Crucially, we show how to build a JIT with Icarus such that verifying the JIT implementation statically ensures the security of all possible programs that the JIT could ever generate at run-time, via a novel technique called symbolic meta-execution that encodes the behaviors of all possible JIT-generated programs as a single Boogie meta-program which can be efficiently verified by SMT solvers. We evaluate Icarus by using it to re-implement components of Firefox's JavaScript JIT. We show that Icarus can scale up to expressing complex JITs, quickly detects real-world JIT bugs and verifies fixed versions, and yields C++ code that is as fast as hand-written code.more » « lessFree, publicly-accessible full text available November 4, 2025
-
Smith, Naomi ; Sharma, Abhishek ; Renner, John ; Thien, David ; Brown, Fraser ; Shacham, Hovav ; Jhala, Ranjit ; Stefan, Deian ( , The 30th ACM Symposium on Operating Systems Principles (SOSP 2024))Free, publicly-accessible full text available September 29, 2025
-
Johnson, Evan ; Thien, David ; Alhessi, Yousef ; Narayan, Shravan ; Brown, Fraser ; Lerner, Sorin ; McMullen, Tyler ; Savage, Stefan ; Stefan, Deian ( , Network and Distributed Systems Security (NDSS) Symposium)null (Ed.)WebAssembly (Wasm) is a platform-independent bytecode that offers both good performance and runtime isolation. To implement isolation, the compiler inserts safety checks when it compiles Wasm to native machine code. While this approach is cheap, it also requires trust in the compiler's correctness---trust that the compiler has inserted each necessary check, correctly formed, in each proper place. Unfortunately, subtle bugs in the Wasm compiler can break---and have broken---isolation guarantees. To address this problem, we propose verifying memory isolation of Wasm binaries post-compilation. We implement this approach in VeriWasm, a static offline verifier for native x86-64 binaries compiled from Wasm; we prove the verifier's soundness, and find that it can detect bugs with no false positives. Finally, we describe our deployment of VeriWasm at Fastly.more » « less