<html><body><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div data-marker="__QUOTED_TEXT__"><div style="font-family: garamond,new york,times,serif; font-size: 12pt; color: #000000"><div>Weikun Yang will present his general exam on Wednesday, May 24, 2017 at 10am in CS 402.<br></div><div><br>The members of his committee are: Aarti Gupta (adviser), Andrew Appel, and Zak Kincaid.<br><br>Everyone is invited to attend his talk and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below.<br></div><div><div class=""><div class=""><br class=""></div><div class="">Lazy Self-Composition for Security Verification</div><div class=""><br class=""></div><div class="">Verification of secure information flow plays an important role in protection of security and privacy in software applications. It can be reduced to safety verification, as shown by Barthe et al., where a “self-composition” of the program is created by duplicating the program on which a safety property is verified. Due to practical challenges of software verification on duplicated copies, Terauchi and Aiken proposed to use type-directed transformation during self-composition. However it relies on static type analysis which can be imprecise. To further reduce the cost of verification, we use an approach based on bounded model checking to encode symbolic and precise propagation of taint, enabling lazy self-composition that duplicates only the tainted parts of the program. Furthermore, we perform additional checks during bounded model checking to enable early termination of security verification, without needing to compute program invariants. We have implemented a prototype information flow checker in the SeaHorn verification platform, which uses Horn-clause based program representations and the Z3 SMT solver in the backend. We present experiments showing effectiveness of our approach on several examples.</div></div><div class=""><br class=""></div><div class=""><br class=""></div><div class="">Research papers:</div><div class=""><div class=""><ol class=""><li class="">Gilles Barthe, Pedro R. D'Argenio, and Tamara Rezk. 2004.<i class=""> Secure Information Flow by Self-Composition</i>. CSFW ’04.</li><li class="">Tachio Terauchi and Alex Aiken. 2005. <i class="">Secure information flow as a safety problem.</i> SAS’05.</li><li class="">Pramod Subramanyan, Sharad Malik, Hareesh Khattri, Abhranil Maiti, and Jason Fung. 2016. <i class="">Verifying information flow properties of firmware using symbolic execution</i>. DATE ’16.</li><li class="">Gilles Barthe, Juan Manuel Crespo, César Kunz. 2011. <i class="">Relational Verification Using Product Programs.</i> FM’11.</li><li class="">Marcelo Sousa and Isil Dillig. 2016.<i class=""> Cartesian hoare logic for verifying k-safety properties.</i> PLDI ’16.</li><li class="">José Bacelar Almeida, Manuel Barbosa, Gilles Barthe, François Dupressoir, Michael Emmi. 2016. <i class="">Verifying constant-time implementations</i>. USENIX’16.</li><li class="">Nikolaj Bjørner, Arie Gurfinkel, Ken McMillan, and Andrey Rybalchenko. 2015. <i class="">Horn Clause Solvers for Program Verification.</i> In Fields of Logic and Computation II. Lecture Notes in Computer Science, vol 9300.</li><li class="">Edward J. Schwartz, Thanassis Avgerinos, and David Brumley. 2010. <i class="">All You Ever Wanted to Know about Dynamic Taint Analysis and Forward Symbolic Execution (but Might Have Been Afraid to Ask)</i>. SP ’10.</li><li class="">A. Sabelfeld and A. C. Myers. 2003. <i class="">Language-based information-flow security.</i> IEEE J.Sel. A. Commun. 21, 1.</li></ol><div class="">and books:</div></div></div><div class=""><ol class=""><li class="">Benjamin C. Pierce. 2002. <i class="">Types and Programming Languages.</i></li><li class="">Aaron R. Bradley and Zohar Manna. 2007. <i class="">The Calculus of Computation: Decision Procedures with Applications to Verification.</i></li></ol></div><div class=""></div></div></div><br></div></div></body></html>