Publications, arranged by date

▶ 2012-2014

• Defining Injection Attacks. Donald Ray and Jay Ligatti. Proceedings of the 17th International Information Security Conference (ISC), October 2014. [BibTeX] This paper defines and analyzes injection attacks. The definition is based on the NIE property, which states that an application's untrusted inputs must only produce Noncode Insertions or Expansions in output programs (e.g., SQL queries). That is, when applications generate output programs based on untrusted inputs, the NIE property requires that inputs only affect output programs by inserting or expanding noncode tokens (e.g., string and float literals, lambda values, pointers, etc). This paper calls attacks based on violating the NIE property BroNIEs (i.e., Broken NIEs) and shows that all code-injection attacks are BroNIEs. In addition, BroNIEs contain many malicious injections that do not involve injections of code; we call such attacks noncode-injection attacks. In order to mitigate both code- and noncode-injection attacks, this paper presents an algorithm for detecting and preventing BroNIEs. [Abstract]
• Fingerprinting Far Proximity from Radio Emissions. Tao Wang, Yao Liu, and Jay Ligatti. Proceedings of the European Symposium on Research in Computer Security (ESORICS), September 2014. [BibTeX] As wireless mobile devices are more and more pervasive and adopted in critical applications, it is becoming increasingly important to measure the physical proximity of these devices in a secure way. Although various techniques have been developed to identify whether a device is close, the problem of identifying the far proximity (i.e., a target is at least a certain distance away) has been neglected by the research community. Meanwhile, verifying the far proximity is desirable and critical to enhance the security of emerging wireless applications. In this paper, we propose a secure far proximity identification approach that determines whether or not a remote device is far away. The key idea of the proposed approach is to estimate the far proximity from the unforgeable "fingerprint" of the proximity. We have validated and evaluated the effectiveness of the proposed far proximity identification method through experiments on real measured channel data. The experiment results show that the proposed approach can detect the far proximity with a successful rate of 0.85 for the non-Line-of-sight (NLoS) scenario, and the successful rate can be further increased to 0.99 for the Line-of-sight (LoS) scenario. [Abstract]
• On Subtyping-Relation Completeness, with an Application to Iso-Recursive Types. Jay Ligatti, Jeremy Blackburn, and Michael Nachtigal. Technical Report. University of South Florida, August 2014. (This is a major revision to technical report CSE-071012, "Completely Subtyping Iso-Recursive Types", from July 2012.) [BibTeX] Well-known techniques exist for proving the soundness of subtyping relations with respect to type safety. However, completeness has not been treated with widely applicable techniques, as far as we're aware.
  
  This paper develops some techniques for stating and proving that a subtyping relation is complete with respect to type safety and applies the techniques to the study of iso-recursive subtyping.
  
  The common subtyping rules for iso-recursive types---the "Amber rules"---are shown to be incomplete with respect to type safety. That is, there exist iso-recursive types t1 and t2 such that t1 can safely be considered a subtype of t2, but t1<=t2 is not derivable with the Amber rules.
  
  This paper defines new, algorithmic rules for subtyping iso-recursive types and proves that the rules are sound and complete with respect to type safety. The fully implemented subtyping algorithm is optimized to run in O(mn) time, where m is the number of mu-terms in the types being considered and n is the size of the types being considered. [Abstract]
• Defining Injection Attacks. Donald Ray and Jay Ligatti. Technical Report CSE-TR-081114. University of South Florida, August 2014. [BibTeX] This paper defines and analyzes injection attacks. The definition is based on the NIE property, which states that an application's untrusted inputs must only produce Noncode Insertions or Expansions in output programs (e.g., SQL queries). That is, when applications generate output programs based on untrusted inputs, the NIE property requires that inputs only affect output programs by inserting or expanding noncode tokens (e.g., string and float literals, lambda values, pointers, etc). This paper calls attacks based on violating the NIE property BroNIEs (i.e., Broken NIEs) and shows that all code-injection attacks are BroNIEs. In addition, BroNIEs contain many malicious injections that do not involve injections of code; we call such attacks noncode-injection attacks. In order to mitigate both code- and noncode-injection attacks, this paper presents an algorithm for detecting and preventing BroNIEs. [Abstract]
• Modeling Runtime Enforcement with Mandatory Results Automata. Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. To appear in the International Journal of Information Security. (preliminary version) [BibTeX]
• Design of Adiabatic Dynamic Differential Logic for DPA-Resistant Secure Integrated Circuits. Matthew Morrison, Nagarajan Ranganathan, and Jay Ligatti. To appear in the IEEE Transactions on Very Large Scale Integration Systems.
• Modeling Runtime Enforcement with Mandatory Results Automata. Egor Dolzhenko, Jay Ligatti, and Srikar Reddy. Technical Report USF-CSE-1213, University of South Florida, December 2013. [BibTeX]
• Induction on Failing Derivations. Jay Ligatti. Technical Report PL-Sep13. University of South Florida, September 2013. [BibTeX] This brief note describes a proof technique called induction on failing derivations. We wish to prove properties of judgments in deductive systems. Standard techniques exist for proving such properties on valid judgments; this note defines a technique for proving such properties on invalid (underivable) judgments. [Abstract]
• Enforcing More with Less: Formalizing Target-aware Run-time Monitors. Yannis Mallios, Lujo Bauer, Dilsun Kaynar, and Jay Ligatti. Proceedings of the International Workshop on Security and Trust Management (STM), September 2012. [BibTeX]
• A Location-based Policy-specification Language for Mobile Devices. Joshua Finnis, Nalin Saigal, Adriana Iamnitchi, and Jay Ligatti. Pervasive and Mobile Computing Journal, Vol 8, No 3, pp 402-414. Elsevier, June 2012. Local version. [BibTeX]
• Defining Code-injection Attacks. Donald Ray and Jay Ligatti. Proceedings of the ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), January 2012. [BibTeX]

▶ 2011

• PoliSeer: A Tool for Managing Complex Security Policies. Daniel Lomsak and Jay Ligatti. Journal of Information Processing, Vol 19, pp 292-306, Information Processing Society of Japan, July 2011. [BibTeX]

▶ 2010

• A Theory of Runtime Enforcement, with Results. Jay Ligatti and Srikar Reddy. Proceedings of the European Symposium on Research in Computer Security (ESORICS), September 2010. [BibTeX]
• A Packet-classification Algorithm for Arbitrary Bitmask Rules, with Automatic Time-space Tradeoffs. Jay Ligatti, Josh Kuhn, and Chris Gage. Proceedings of the IEEE International Conference on Computer Communication Networks (ICCCN), August 2010. [BibTeX]
• PoliSeer: A Tool for Managing Complex Security Policies. Daniel Lomsak and Jay Ligatti. Proceedings of the International Conference on Trust Management (IFIP-TM), June 2010. [BibTeX]
• A Theory of Runtime Enforcement, with Results. Jay Ligatti and Srikar Reddy. Technical Report USF-CSE-SS-102809, University of South Florida, October 2009, revised June 2010. [BibTeX]

▶ 2009

• PoliSeer: A Tool for Managing Complex Security Policies. Daniel Lomsak and Jay Ligatti. Technical Report CSE-SSec-112509, University of South Florida, November 2009. [BibTeX]
• IVCon: Inline Visualization of Concerns. Nalin Saigal and Jay Ligatti. Technical Report CSE-110909-SE, University of South Florida, November 2009. [BibTeX]
• Control-Flow Integrity: Principles, Implementations, and Applications. Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. ACM Transactions on Information and System Security, Vol 13, No 1, pp 1-40. ACM Press, October 2009. Local version. [BibTeX]
• Inline Visualization of Concerns. Nalin Saigal and Jay Ligatti. Proceedings of the ACIS International Conference on Software Engineering Research, Management, and Applications (SERA), December 2009. [BibTeX]
• LoPSiL: A Location-based Policy-specification Language. Jay Ligatti, Billy Rickey, and Nalin Saigal. Proceedings of the International ICST Conference on Security and Privacy in Mobile Information and Communication Systems (MobiSec), June 2009. [BibTeX]
• Composing Expressive Runtime Security Policies. Lujo Bauer, Jay Ligatti, and David Walker. ACM Transactions on Software Engineering and Methodology, Vol 18, No 3, pp 1-43. ACM Press, May 2009. Local version. [BibTeX]
• Run-Time Enforcement of Nonsafety Policies. Jay Ligatti, Lujo Bauer, and David Walker. ACM Transactions on Information and System Security, Vol 12, No 3, pp 1-41. ACM Press, January 2009. Local version. [BibTeX]

▶ 2008

• Defining and Visualizing Many-to-many Relationships between Concerns and Code. Nalin Saigal and Jay Ligatti. Technical Report CSE-090608-SE, University of South Florida, September 2008. [BibTeX]

▶ 2007

• Fault-tolerant Typed Assembly Language. Frances Perry, Lester Mackey, George Reis, Jay Ligatti, David August, and David Walker. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2007. [BibTeX]
• Fault-tolerant Typed Assembly Language. Frances Perry, Lester Mackey, George Reis, Jay Ligatti, David August, and David Walker. Technical Report TR-776-07, Princeton University, April 2007. [BibTeX]

▶ 2006

• A Type-theoretic Interpretation of Pointcuts and Advice. Jay Ligatti, David Walker, and Steve Zdancewic. Science of Computer Programming: Special Issue on Foundations of Aspect-Oriented Programming, Vol 63, No 3, pp 240-266. Elsevier, December 2006. Local version. [BibTeX]
• Static Typing for a Faulty Lambda Calculus. David Walker, Lester Mackey, Jay Ligatti, George Reis, and David August. Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP), September 2006. [BibTeX]
• Policy Enforcement via Program Monitoring. Jarred Adam Ligatti. PhD thesis, Princeton University, June 2006. [BibTeX]

▶ 2005

• Control-Flow Integrity: Principles, Implementations, and Applications. Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Proceedings of the ACM SIGSAC Conference on Computer and Communications Security (CCS), November 2005. [BibTeX]
• A Theory of Secure Control Flow. Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Proceedings of the 7th International Conference on Formal Engineering Methods (ICFEM), November 2005. [BibTeX]
• Enforcing Non-safety Security Policies with Program Monitors. Jay Ligatti, Lujo Bauer, and David Walker. Proceedings of the 10th European Symposium on Research in Computer Security (ESORICS), September 2005. [BibTeX]
• Composing Security Policies with Polymer. Lujo Bauer, Jay Ligatti, and David Walker. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2005. [BibTeX]
• Control-Flow Integrity. Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Technical Report MSR-TR-2005-18, Microsoft Research, February 2005 (revised June 2005). [BibTeX]
• A Theory of Secure Control Flow. Martin Abadi, Mihai Budiu, Ulfar Erlingsson, and Jay Ligatti. Technical Report MSR-TR-2005-17, Microsoft Research, February 2005 (revised June 2005). [BibTeX]
• Enforcing Non-safety Security Policies with Program Monitors. Jay Ligatti, Lujo Bauer, and David Walker. Technical Report TR-720-05, Princeton University, January 2005 (revised June 2005). [BibTeX]
• Edit Automata: Enforcement Mechanisms for Run-time Security Policies. Jay Ligatti, Lujo Bauer, and David Walker. International Journal of Information Security, Vol 4, No 1-2, pp 2-16. Springer-Verlag, Feb 2005. Local Version. [BibTeX]

▶ 2004

• A Language and System for Composing Security Policies. Lujo Bauer, Jay Ligatti, and David Walker. Technical Report TR-699-04, Princeton University, January 2004. [BibTeX]

▶ 2003

• Types and Effects for Non-interfering Program Monitors. Lujo Bauer, Jarred Ligatti, and David Walker. In M. Okada, B. Pierce, A. Scedrov, H. Tokuda, and A. Yonezawa, editors, Lecture Notes in Computer Science: Software Security - Theories and Systems (Revised Papers of the 2002 Mext-NSF-JSPS International Symposium), Vol 2609, pp 154-171. Springer-Verlag, November 2003. [BibTeX]
• A Theory of Aspects. David Walker, Steve Zdancewic, and Jay Ligatti. Proceedings of the ACM SIGPLAN International Conference on Functional Programming (ICFP), August 2003. [BibTeX]
• Edit Automata: Enforcement Mechanisms for Run-time Security Policies. Jay Ligatti, Lujo Bauer, and David Walker. Princeton University Technical Report TR-681-03, May 2003. [BibTeX]

▶ 2002

• A Calculus for Composing Security Policies. Lujo Bauer, Jarred Ligatti, and David Walker. Technical Report TR-655-02, Princeton University, August 2002. [BibTeX]
• More Enforceable Security Policies. Lujo Bauer, Jarred Ligatti, and David Walker. Foundations of Computer Security Workshop (FCS) '02 (associated with LICS '02), July 2002. [BibTeX]
• More Enforceable Security Policies. Lujo Bauer, Jarred Ligatti, and David Walker. Technical Report TR-649-02, Princeton University, July 2002. [BibTeX]