[mathetic]

Sorry, I didn't mean to mislead. I was exemplifying ways of subtly leaking data. In the next paragraph, I clarify what we cover with the following:

> Namely, we implement a type system that regulates explicit and implicit dataflows as well as non-termination as a covert channel.

Yes, there is work on preventing timing attacks using static types. One is "A Hardware Design Language for Timing-Sensitive Information-Flow Security" which addresses exactly this problem. The second line of work is resource analysis. There are type systems that can specify the complexity of the program. Check out for example relational cost analysis [0]. This can be used for privacy and security purposes.

Needless to say, this is considerably more sophisticated than what I covered.

[0] https://dl.acm.org/doi/10.1145/2694344.2694372 [1] https://dl.acm.org/doi/10.1145/3009837.3009858