2 ms·
> All possible execution sequences must ensure to satisfy all possible cross-interaction rules to not make any time channel visible Does this refer to some the
by nextaccountic 3y ago
> All possible execution sequences must ensure to satisfy all possible cross-interaction rules to not make any time channel visible
Does this refer to some theorem? I'm very interested in how to model & prove formally that a given operation on a given system doesn't have timing side channels
- matu3ba 3y agoI know of TCF from https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.pdf https://www.cs.yale.edu/homes/antonopoulos-timos/PLDI-2017.p..., but the folks from sel4 have likely improved the models as they have a full research team on it: https://trustworthy.systems/projects/TS/timeprotection/ https://trustworthy.systems/projects/TS/timeprotection/. You might want to get involved.