Skip to content

WIP : Yield isolation proof

Florian Vanhems requested to merge yield_isolation_proof into main

This branch adds a formal isolation proof preservation of the yield service, with minimal additions to the model. As a result, most of the code that indeed modifies the state is not at all integrated in the model. The most obvious and critical piece of code that is not modeled properly is the writeContext function that writes an execution context inside a partition's accessible memory. Currently this function does nothing in the model.

Edited by Florian Vanhems

Merge request reports