Information-flow control on ARM and POWER multicore processors

DOI10.1007/S10703-021-00376-2zbMATH Open1505.68001OpenAlexW3167089364MaRDI QIDQ2147697FDOQ2147697

Yanyan Li

Publication date: 20 June 2022

Published in: Formal Methods in System Design (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/s10703-021-00376-2

zbMATH Keywords

weak memory modelsinformation-flow securitynon-blocking algorithms

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Mathematical problems of computer architecture (68M07)

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• An axiomatic basis for computer programming
• Tools and algorithms for the construction and analysis of systems. 14th international conference, TACAS 2008, held as part of the joint European conferences on theory and practice of software, ETAPS 2008, Budapest, Hungary, March 29--April 6, 2008. Proceedings
• A wide-spectrum language for verification of programs on weak memory models
• A promising semantics for relaxed-memory concurrency
• The verified CakeML compiler backend
• Dependent information flow types
• Title not available (Why is that?)
• Information Security and Cryptology - ICISC 2005

Uses Software

• Isabelle/HOL
• z3
• CompCert

This page was built for publication: Information-flow control on ARM and POWER multicore processors

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2147697)