I found this paper interesting: (https://www.trojansource.codes/trojan-source.pdf) - it describes how to inject invisible (skipping reviews) source code using unicode tricks - any compiler accepting full Unicode input should be vulnerable to this (I created issues for coqc, ocaml and CompCert to have this checked).
see also discussion here which mentioned the authors' info page for this paper: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Finding.20an.20old.20Coq-club.20post.20on.20Pollack.20inconsistency.3F
Thanks - I didn't know the term "Pollack inconsistency" and didn't associate it with this.
Last updated: Nov 29 2023 at 06:01 UTC