Verifying components of Arm(R) Confidential Computing Architecture with ESBMC

Autor: Wu, Tong, Xiong, Shale, Manino, Edoardo, Stockwell, Gareth, Cordeiro, Lucas C.

Realm Management Monitor (RMM) is an essential firmware component within the recent Arm Confidential Computing Architecture (Arm CCA). Previous work applies formal techniques to verify the specification and prototype reference implementation of RMM.

Externí odkaz: http://arxiv.org/abs/2406.04375

Private delegated computations using strong isolation

Autor: Brossard, Mathias, Bryant, Guilhem, Gaabouri, Basma El, Fan, Xinxin, Ferreira, Alexandre, Grimley-Evans, Edmund, Haster, Christopher, Johnson, Evan, Miller, Derek, Mo, Fan, Mulligan, Dominic P., Spinale, Nick, van Hensbergen, Eric, Vincent, Hugo J. M., Xiong, Shale

Sensitive computations are now routinely delegated to third-parties. In response, Confidential Computing technologies are being introduced to microprocessors, offering a protected processing environment, which we generically call an isolate, providin

Externí odkaz: http://arxiv.org/abs/2205.03322

Tento výsledek nelze pro nepřihlášené uživatele zobrazit.
K zobrazení výsledku je třeba se přihlásit.

Data Consistency in Transactional Storage Systems: {A} Centralised Semantics

Autor: Xiong, Shale, Cerone, Andrea, Raad, Azalea, Gardner, Philippa

Publikováno v: European Conference on Object-Oriented Programming (ECOOP)
34th European Conference onObject-Oriented Programming
Leibniz International Proceedings in Informatics

We introduce an interleaving operational semantics for describing the client-observable behaviour of atomic transactions on distributed key-value stores. Our semantics builds on abstract states comprising centralised, global key-value stores and part

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d6abd57bf4c9a3e378d0482a1445dab7