Zobrazeno 1 - 10
of 37
pro vyhledávání: '"Chris Hawblitzel"'
Autor:
Chris Hawblitzel, Erez Petrank
Publikováno v:
Logical Methods in Computer Science, Vol Volume 6, Issue 3 (2010)
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the p
Externí odkaz:
https://doaj.org/article/bd248fd82f6c46b4a48f3c3da8a80c54
Autor:
Andrea Lattuada, Travis Hance, Chanhee Cho, Matthias Brun, Isitha Subasinghe, Yi Zhou, Jon Howell, Bryan Parno, Chris Hawblitzel
Publikováno v:
Proceedings of the ACM on Programming Languages, 7 (OOPSLA1)
The Rust programming language provides a powerful type system that checks linearity and borrowing, allowing code to safely manipulate memory without garbage collection and making Rust ideal for developing low-level, high-assurance systems. For such s
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::1de56667119ea7550a98d291dddc285d
https://doi.org/10.1145/3586037
https://doi.org/10.1145/3586037
Autor:
Jialin Li, Andrea Lattuada, Yi Zhou, Jonathan Cameron, Jon Howell, Bryan Parno, Chris Hawblitzel
Publikováno v:
Proceedings of the ACM on Programming Languages, 6 (OOPSLA1)
Reasoning about memory aliasing and mutation in software verification is a hard problem. This is especially true for systems using SMT-based automated theorem provers. Memory reasoning in SMT verification typically requires a nontrivial amount of man
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::5d86c9083717263fc9bd5482f071e105
https://doi.org/10.1145/3527313
https://doi.org/10.1145/3527313
Autor:
Aseem Rastogi, Bryan Parno, Aymeric Fromherz, Chris Hawblitzel, Nikhil Swamy, Nick Giannarakis
Publikováno v:
Proceedings of the ACM on Programming Languages. 3:1-30
High-performance cryptographic libraries often mix code written in a high-level language with code written in assembly. To support formally verifying the correctness and security of such hybrid programs, this paper presents an embedding of a subset o
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::9c88f32b3bd2ba3fff9e7d1ba0fdb9fe
https://doi.org/10.1145/3290376
https://doi.org/10.1145/3290376
Autor:
Nikhil Swamy, Antoine Delignat-Lavaud, Jonathan Protzenko, Joonwon Choi, Bryan Parno, Christoph M. Wintersteiger, Chris Hawblitzel, Aseem Rastogi, Natalia Kulatova, Aymeric Fromherz, Marina Polubelova, Santiago Zanella-Béguelin, Tahina Ramananandro, Karthikeyan Bhargavan, Benjamin Beurdouche, Cédric Fournet
Publikováno v:
SP 2020-IEEE Symposium on Security and Privacy
SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩
IEEE Symposium on Security and Privacy
2020 IEEE Symposium on Security and Privacy (SP)
SP 2020-IEEE Symposium on Security and Privacy, May 2020, San Francisco / Virtual, United States. pp.983-1002, ⟨10.1109/SP40000.2020.00114⟩
IEEE Symposium on Security and Privacy
2020 IEEE Symposium on Security and Privacy (SP)
International audience; We present EverCrypt: a comprehensive collection of verified, high-performance cryptographic functionalities available via a carefully designed API. The API provably supports agility (choosing between multiple algorithms for t
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::b754b12d09129b9fb446c4bb80a284b0
https://inria.hal.science/hal-03154278
https://inria.hal.science/hal-03154278
Publikováno v:
Lecture Notes in Computer Science ISBN: 9783030636173
VSTTE
VSTTE
Hand-optimized assembly language code is often difficult to formally verify. This paper combines Hoare logic with verified code transformations to make it easier to verify such code. This approach greatly simplifies existing proofs of highly optimize
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::b128202ca9ac2d1537c35bf9899a6202
https://doi.org/10.1007/978-3-030-63618-0_7
https://doi.org/10.1007/978-3-030-63618-0_7
Autor:
Chris Hawblitzel
Publikováno v:
Electronic Proceedings in Theoretical Computer Science. 307:3-5
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::a62de863c04f94cdfe8bf3188234c11d
https://doi.org/10.4204/eptcs.307.1
https://doi.org/10.4204/eptcs.307.1
Autor:
Michael L. Roberts, Manos Kapritsos, Bryan Parno, Chris Hawblitzel, Srinath Setty, Jon Howell, Jacob R. Lorch, Brian Zill
Publikováno v:
Communications of the ACM. 60:83-92
Distributed systems are notorious for harboring subtle bugs. Verification can, in principle, eliminate these bugs, but it has historically been difficult to apply at full-program scale, much less distributed system scale. We describe a methodology fo
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::c01ad58af6e95ac2cc6b8bbaca8b92d0
https://doi.org/10.1145/3068608
https://doi.org/10.1145/3068608
Publikováno v:
SOSP
Intel SGX promises powerful security: an arbitrary number of user-mode enclaves protected against physical attacks and privileged software adversaries. However, to achieve this, Intel extended the x86 architecture with an isolation mechanism approach
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_________::6f1ae219ef212af4944404c96660534d
https://doi.org/10.1145/3132747.3132782
https://doi.org/10.1145/3132747.3132782
Autor:
Chris Hawblitzel, Erez Petrank
Publikováno v:
POPL
Garbage collectors are notoriously hard to verify, due to their low-level interaction with the underlying system and the general difficulty in reasoning about reachability in graphs. Several papers have presented verified collectors, but either the p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::a2782996ccb8fc1aedd48c857a818ab3
https://doi.org/10.1145/1594834.1480935
https://doi.org/10.1145/1594834.1480935