Research Interests

My research interest lies in Computer Security and Privacy. Broadly, I am interested in applying techniques from formal verification and runtime monitoring in achieving provable security and privacy assurances of modern systems and protocols. I am also interested in applying formal verification and software engineering techniques to automatically detect functional bugs in network protocols and safety-critical cyber-physical and IoT systems.

Research Interests (Keywords)

Computer Security, Privacy, Formal Methods, Automated Reasoning

Selected Publications

• An Empirical Study of Mnemonic Sentence-based Password Generation Strategies
  With Weining Yang, Ninghui Li, Aiping Xiong, and Robert Proctor
  Appeared in the Proceeding of 23rd ACM Conference on Computer and Communications Security (CCS), 2016. 
• On the Security and Usability of Segment-based Visual Cryptographic Authentication Protocols
  With Tianhao Wang, Huangyi Ge, Hemanta K. Maji, and Ninghui Li
  Appeared in the Proceeding of 23rd ACM Conference on Computer and Communications Security (CCS), 2016. 
• Tri-Modularization of Firewall Policies
  With Haining Chen, Ninghui Li, Warut Khern-am-nuai, Suresh Chari, Ian Molloy, and Youngja Park
  Appeared in the Proceeding of 21st ACM on Symposium on Access Control Models and Technologies (SACMAT), 2016. 
• Equivalence-based Security for Querying Encrypted Databases: Theory and Application to Privacy Policy Audits
  With Deepak Garg, Limin Jia, and Anupam Datta
  Appeared in the Proceeding of 22nd ACM Conference on Computer and Communications Security (CCS), 2015. 
• A Case Study on Runtime Monitoring of an Autonomous Research Vehicle (ARV) System
  With Aaron Kane, Anupam Datta, and Philip Koopman
  Appeared in the Proceedings of 15th International Conference on Runtime Verification (RV), 2015. 
• Temporal Mode-Checking for Runtime Monitoring of Privacy Policies
  With Limin Jia, Deepak Garg, and Anupam Datta
  Appeared in the Proceedings of 26th International Conference on Computer Aided Verification (CAV), 2014. 
• Privacy Promises That Can Be Kept: A Policy Analysis Method with Application to the HIPAA Privacy Rule
  With Andreas Gampe, Jianwei Niu, Jeffery von Ronne, Jared Bennatt, Anupam Datta, Limin Jia, and William H. Winsborough
  Appeared in the Proceedings of the 18th ACM symposium on Access control models and technologies (SACMAT), 2013. 
• On XACML's Adequacy to Specify and to Enforce HIPAA
  With Haining Chen, Jianwei Niu, Ninghui Li, and Elisa Bertino
  Appeared in the Proceedings of the 3rd USENIX Workshop on Health Security and Privacy (HealthSec), 2012.
• Ensuring Authorization Privileges for Cascading User Obligations Best Paper Award 
  With Murillo Pontual, William H. Winsborough, Ting Yu, Keith Irwin, and Jianwei Niu
  Appeared in the Proceedings of the 17th ACM symposium on Access control models and technologies (SACMAT), 2012. 
• The Privacy in the Time of the Internet: Secrecy vs Transparency 
  With Murillo Pontual, Andreas Gampe, Bazoumana Kone, Md Shamim Ashik, and William H. Winsborough
  Appeared in the second ACM conference on Data and Application Security and Privacy (CODASPY), 2012.