We are presented with a big zip file of SML code, which implements an interpreter for a small ML-like language with a form of taint analysis in its type checker, called Wolf. Concretely, every type in Wolf’s type system has an associated secrecy: it is either “private” or “public”, and in theory, the type system makes it impossible to do any computation on private data to get a public result.

In doggo (the sequel to pupper), if statements are properly analyzed and the taint analysis is extended to also include the purity of expressions and functions. However, doggo's clever way of keeping track of the purity of functions interacts poorly with coercion, allowing us to perform side effects where we shouldn't be able to and exfiltrate bits of the flag.

https://blog.vero.site/post/doggo