MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code

Autor: Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya, Evan Johnson, Aidan Denlinger, Craig Disselkoen, Conrad Watt, Bryan Parno, Marco Patrignani, Marco Vassena, Deian Stefan

Publikováno v: Proceedings of the ACM on Programming Languages. 7:425-454

Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm—and attackers can exploit buffer overflows and use-after-frees in Wasm almos

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::5de77d7b777bbee4c67c1b1de8fd1e40
https://doi.org/10.1145/3571208

Isolation Without Taxation: {N}ear-Zero-Cost Transitions for {WebAssembly} and {SFI}

Autor: Matthew Kolosick, Shravan Narayan, Evan Johnson, Conrad Watt, Michael LeMay, Deepak Garg, Ranjit Jhala, Deian Stefan

Publikováno v: Proceedings of the ACM on Programming Languages
49th ACM SIGPLAN Symposium on Principles of Programming Languages

Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to harden the Firefox browser by sandboxing third-party libraries, and compan

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::cc0edfeb948570db2ec2803d07929dbf
https://hdl.handle.net/21.11116/0000-0009-B26B-621.11116/0000-0009-CB9F-021.11116/0000-0009-B269-8

Solver-Aided Constant-Time Hardware Verification

Autor: Klaus von Gleissenthall, Deian Stefan, Ranjit Jhala, Rami Gökhan Kıcı

Publikováno v: CCS
von Gleissenthall, K, Klcl, R G, Stefan, D & Jhala, R 2021, Solver-Aided Constant-Time Hardware Verification . in CCS 2021 : Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security . Proceedings of the ACM Conference on Computer and Communications Security, vol. 2021, Association for Computing Machinery, pp. 429-444, 27th ACM Annual Conference on Computer and Communication Security, CCS 2021, Virtual, Online, Korea, Republic of, 15/11/21 . https://doi.org/10.1145/3460120.3484810
CCS 2021: Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security, 429-444
STARTPAGE=429;ENDPAGE=444;TITLE=CCS 2021

We present Xenon, a solver-aided, interactive method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing the effort needed to localize the root cause of verificati

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::af858411b27c9ac547e3c199a2642396
https://doi.org/10.1145/3460120.3484810

Scooter & Sidecar: a domain-specific approach to writing secure database migrations

Autor: Deian Stefan, Fraser Brown, Sorin Lerner, Alex Sanchez-Stern, John Renner

Publikováno v: PLDI

Web applications often handle large amounts of sensitive user data. Modern secure web frameworks protect this data by (1) using declarative languages to specify security policies alongside database schemas and (2) automatically enforcing these polici

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::1a0ca4f60ff00ec598cf4d46367f4246
https://doi.org/10.1145/3453483.3454072

Pretend synchrony: synchronous verification of asynchronous distributed programs

Autor: Ranjit Jhala, Rami Gökhan Kıcı, Alexander Bakst, Klaus von Gleissenthall, Deian Stefan

Publikováno v: Proceedings of the ACM on Programming Languages, 3(POPL):59, 1-30. Association for Computing Machinery (ACM)
von Gleissenthal, K, Klcl, R G, Bakst, A, Stefan, D & Jhala, R 2019, ' Pretend synchrony: synchronous verification of asynchronous distributed programs ', Proceedings of the ACM on Programming Languages, vol. 3, no. POPL, 59, pp. 1-30 . https://doi.org/10.1145/3290372

We present pretend synchrony , a new approach to verifying distributed systems, based on the observation that while distributed programs must execute asynchronously, we can often soundly treat them as if they were synchronous when verifying their cor

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4d90e94a209ddcd3712755180e50c2c8
https://research.vu.nl/en/publications/f0a33e44-6120-41fd-9dce-e33b26b5b3ca