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

Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade

Autor: Sunjay Cauligi, Marco Vassena, Ranjit Jhala, Dean M. Tullsen, Deian Stefan, Craig Disselkoen, Rami Gökhan Kıcı, Klaus von Gleissenthall

Publikováno v: Vassena, M, Disselkoen, C, von Gleissenthall, K, Cauligi, S, Klcl, R G, Jhala, R, Tullsen, D & Stefan, D 2021, ' Automatically eliminating speculative leaks from cryptographic code with blade ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 49, pp. 1-30 . https://doi.org/10.1145/3434330
Proceedings of the ACM on Programming Languages, 5(POPL):49, 1-30. Association for Computing Machinery (ACM)

We introduce Blade, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. Blade is built on the insight that to stop leaks via speculative execution, it suffices to cut the dataflow from expressions that

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::603a7cd743d1a11259db2d4e6c7c1be1
http://arxiv.org/abs/2005.00294

Towards Automated Proving of Relational Properties of Probabilistic Programs (Invited Talk)

Autor: Andrey Rybalchenko, Klaus von Gleissenthall, Santiago Zanella-Béguelin

Publikováno v: VPT@CAV

Some security properties go beyond what is expressible in terms of anindividual execution of a single program. In particular, many securitypolicies in cryptography can be naturally phrased as relationalproperties of two open probabilistic programs. W

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::17b3c250bba84f93f76437980f097031
https://doi.org/10.29007/t2h1

Symbolic Polytopes for Quantitative Interpolation and Verification

Autor: Klaus von Gleissenthall, Boris Köpf, Andrey Rybalchenko

Publikováno v: Computer Aided Verification ISBN: 9783319216898
CAV (1)
Computer Aided Verification-27th International Conference
von Gleissenthal, K, Köpf, B & Rybalchenko, A 2015, Symbolic Polytopes for Quantitative Interpolation and Verification . in Computer Aided Verification-27th International Conference . Springer LNCS . < https://link.springer.com/chapter/10.1007/978-3-319-21690-4_11 >

Proving quantitative properties of programs, such as bounds on resource usage or information leakage, often leads to verification conditions that involve cardinalities of sets. Existing approaches for dealing with such verification conditions operate

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::81cfafc56956aeb5f3875de6b03b4a72
https://doi.org/10.1007/978-3-319-21690-4_11

An Epistemic Perspective on Consistency of Concurrent Computations

Autor: Klaus von Gleissenthall, Andrey Rybalchenko

Publikováno v: CONCUR 2013 – Concurrency Theory ISBN: 9783642401831
CONCUR

Consistency properties of concurrent computations, e.g., sequential consistency, linearizability, or eventual consistency, are essential for devising correct concurrent algorithms. In this paper, we present a logical formalization of such consistency

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_________::4ece90ace31bbac968c9d8c82b482388
https://doi.org/10.1007/978-3-642-40184-8_16