Stephen Magill

Research Lead, Software Analysis

My research interests focus on static and dynamic program analysis, with a particular emphasis on scalability and tuning analyses for specific software domains. My recent work focuses on security, both software security in the traditional sense and related issues such as privacy. I have also worked on analyses that help programmers build and deploy software updates in high-availability environments.

Background

Prior to joining Galois in 2014, Stephen was a Research Scientist at the Institute for Defense Analyses Center for Computing Sciences (IDA/CCS). Before that, he was a post-doctoral researcher with Michael Hicks at the University of Maryland, College Park, where his work primarily focused on two topics: 1) verifying correctness of software updates, and 2) enforcing privacy by reasoning statically about accumulated attacker knowledge.

Stephen earned his Ph.D. in Computer Science from Carnegie Mellon University under the guidance of Peter Lee, Stephen Brookes, and John Reynolds. His thesis work developed the theory and implementation of the use of separation logic to produce numeric abstractions of programs. These abstractions can be used to prove termination and other liveness properties of heap-manipulating programs.

Journal Publications

  • Piotr Mardziel, Stephen Magill, Michael Hicks, and Mudhakar Srivatsa. “Dynamic Enforcement of Knowledge-based Security Policies using Probabilistic Abstract Interpretation,” Journal of Computer Security (JCS), 21:463-532, October 2013.

Conference Publications

  • Stephen Magill, Michael Hicks, Suriya Subramanian, and Kathryn S. McKinley. “Automating Object Transformations for Dynamic Software Updating,” ACM Conference on Object-Oriented Programming Languages, Systems, and Applications (OOPSLA), October 2012.
  • Christopher M. Hayden, Stephen Magill, Michael Hicks, Nate Foster, and Jeffrey S. Foster. “Specifying and Verifying the Correctness of Dynamic Software Updates,” International Conference on Verified Software: Theories, Tools, and Experiments (VSTTE), 2012.
  • Piotr Mardziel, Stephen Magill, Michael Hicks, and Mudhakar Srivatsa. “Dynamic Enforcement of Knowledge-based Security Policies,” Computer Security Foundations (CSF), 2011.
  • Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay. “Automatic Numeric Abstractions for Heap-Manipulating Programs,” ACM Symposium on Principles of Programming Languages (POPL), 2010.
  • Byron Cook, Ashutosh Gupta, Stephen Magill, Andrey Rybalchenko, Ji?í Šimša, Satnam Singh, and Viktor Vafeiadis. “Finding heap-bounds for hardware synthesis,” Formal Methods in Computer-Aided Design (FMCAD), 2009.
  • Stephen Magill, Ming-Hsien Tsai, Peter Lee, and Yih-Kuen Tsay, “THOR: A Tool for Reasoning about Shape and Arithmetic,” Conference on Computer Aided Verification (CAV), 2008.
  • Stephen Magill, Josh Berdine, Edmund Clarke, and Byron Cook, “Arithmetic Strengthening for Shape Analysis,” 14th International Static Analysis Symposium (SAS), 2007.
  • Kevin Donnelly, Tyler Gibson, Neel Krishnaswami, Stephen Magill, Sungwoo Park, “The Inverse Method for the Logic of Bunched Implications,” 11th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), 2004.
  • Stephen Magill, Bradley Skaggs, Mauricio Papa and John Hale, “Implementation and verification of programmable security,” 16th International Conference on Data and Applications Security (DBSec), 2002.
  • Mauricio Papa, Oliver Bremer, Stephen Magill, John Hale and Sujeet Shenoi, “Simulation and analysis of cryptographic protocols,” in 14th International Conference on Database Security (DBSec), 2000.
  • Stephen Magill, Brandon Enochs, Dominic Schulte, Clinton Campbell, Gavin Manes and John Hale, “A digital economy simulator,” Proceedings of the Fifth International Conference on Computer Science and Informatics (JCIS 2000), Atlantic City, NJ, pp. 474-475, 2000.

Workshop Publications

  • Stephen Magill, Aleksandar Nanevski, Edmund Clarke, Peter Lee, “Inferring Invariants in Separation Logic for Imperative List-processing Programs,” Third Workshop on Semantics, Program Analysis, and Computing Environments for Memory Management (SPACE), 2006.
  • B. Skaggs, S. Magill, M. Papa, J. Hale and S. Shenoi, “Security service extensions for Java,” Proceedings of the 2001 IEEE Workshop on Information Assurance and Security, United States Military Academy, West Point, NY, pp. 46-53, 2001.