François Dupressoir

`declassified_out` annotations are trusted and are part of the model. By annotating the span of `out` as `declassified_out`, you are telling ct-verif to consider as leakage only differences in execution...

Sorry, I also missed some other details of your example. Can you confirm that you are worried about intermediate values of `out` being observed by the adversary rather than the...

These are issues with the version of Smack you are using not being able to parse more complex annotations. I realise that you cannot upgrade because of the fact that...

Hi @michael-emmi. It did not, but that was mainly due to the fact that we had no annotation language for it. If Smack now eats these annotations and preserves them...

Thanks John. The setup for ct-verif is not robust, and requires very precise versions of llvm and smack, and possibly of bam as well. A student of mine recently put...

MacSlow implemented some gpm-like mouse support a few months back: https://github.com/dvdhrm/kmscon/issues/99#issuecomment-1433552507 Given the work was done on a sibling fork, I don't imagine a rebase will be particularly straightforward, but...