Andrei Sabelfeld, David Sands: A Per Model of Secure Information Flow in Sequential Programs. High. Order Symb. Comput. 14(1): 59-91 (2001)