Complete Publications

Journal Publications

Patrick Traynor, Michael Chien, Scott Weaver, Boniface Hicks, and Patrick McDaniel. Non-Invasive Methods for Host Certification. ACM Transactions on Information and System Security (TISSEC), 11(3), 2008. [ bib ]

Moreno Falaschi, Patrick Hicks, and William Winsborough. Demand transformation analysis for concurrent constraint programs. Journal of Logic Programming, 41(3):185-215, March 2000. [ bib | .pdf ]

This paper presents a demand transformation analysis that maps a predicate's output demands to its input demands. This backward dataflow analysis for concurrent constraint programs is constructed in the framework of abstract interpretation. In the context of stream parallelism, this analysis identifies an amount of input data for which predicate execution can safely wait without danger of introducing deadlock. We assume that programs are well-moded and prove that our analysis is safe. We have constructed an implementation of this analysis and tested it on some small, illustrative programs and have determined that it gives useful results in practice. We identify several applications of the analysis results to distributed implementations of concurrent constraint languages, including thread construction and communication granularity. This analysis will enable exisiting computation cost estimation analyses to be applied to stream-parallel logic languages.

John Hannan and Patrick Hicks. Higher-order uncurrying. Journal of Higher Order and Symbolic Computation, 13(3):179-216, 2000. [ bib | .pdf ]

We present a formal specification of unCurrying for a higher-order, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions that are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function, rather than only unCurrying all of a function's parameters. We present the specification as a deductive system that axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, that implements unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a richer form of unCurrying than is currently found in compilers for functional languages.

Conference and Workshop Publications

Boniface Hicks, Dave King, and Patrick McDaniel. Jifclipse: Development tools for security-typed applications. In Michael Hicks, editor, Proceedings of the 2nd ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS '07), San Diego, CA, June 14 2007. ACM Press. [ bib | http | .pdf ]

Security-typed languages such as Jif require the programmer to label variables with information flow security policies as part of application development. The compiler then flags errors wherever information leaks may occur. Resolving these information leaks is a critical task in security-typed language application development. Unfortunately, because information flows can be quite subtle, simple error messages tend to be insufficient for finding and resolving the source of information leaks; more sophisticated development tools are needed for this task. To this end we provide a set of principles to guide the development of such tools. Furthermore, we implement a subset of these principles in an integrated development environment (IDE) for Jif, called Jifclipse, which is built on the Eclipse extensible development platform. Our plug-in provides a Jif programmer with additional tools to view hidden information generated by a Jif compilation, to suggest fixes for errors, and to get more specific information behind an error message. Better development tools are essential for making security-typed application development practical; Jifclipse is a first step in this process.

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel. Integrating selinux with security-typed languages. In Proceedings of the 3rd SELinux Symposium, Baltimore, MD, USA, March 2007. [ bib | .pdf | .pdf ]

Recent advances in the area of security-typed languages have enabled the development of realistic applications aware of information flow security. Traditionally, operating systems have enforced MAC with minimal dependence on application programs. Although these approaches have common goals, they have progressed independently. However, there are many cases where systems depend on user-level programs to enforce information flows, so integration of information flow enforcement between the operating systems and security-typed applications would be beneficial. In this paper, we examine what it takes to integrate information flow enforcement of a security-typed extension of Java with SELinux. We find that SELinux has most of the necessary features to build a proof-of-concept system, but other services are necessary, such as verifying compliance between information flow policies. Ultimately, we are optimistic that the comprehensive access control enforcement of SELinux will be ideal for integration with these security-typed applications.

Keywords: Information Flow Policies, Java Information Flow (Jif), security-typed languages, SELinux

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel. From trusted to secure: Building and executing applications that enforce system security. In Proceedings of the USENIX Annual Technical Conference, Santa Clara, CA, USA, June 2007. [ bib | .html | .pdf ]

Commercial operating systems have recently introduced mandatory access controls (MAC) that can be used to ensure system-wide data confidentiality and in- tegrity. These protections rely on restricting the flow of information between processes based on security levels. The problem is, there are many applications that defy sim- ple classification by security level, some of them essential for system operation. Surprisingly, the common practice among these operating systems is simply to mark these applications as “trusted”, and thus allow them to bypass label protections. This compromise is not a limitation of MAC or the operating system services that enforce it, but simply a fundamental inability of any operating sys- tem to reason about how applications treat sensitive data internally-and thus the OS must either restrict the data that they receive or trust them to handle it correctly. These practices were developed prior to the advent security-typed languages. These languages provide a means of reasoning about how the OS's sensitive data is handled within applications. Thus, applications can be shown to enforce system security by guaranteeing, in ad- vance of execution, that they will adhere to the OS's MAC policy. In this paper, we provide an architecture for an op- erating system service, that integrate security-typed lan- guage with operating system MAC services. We have built an implementation of this service, called SIESTA, which handles applications developed in the security-typed lan- guage, Jif, running on the SELinux operating system. We also provide some sample applications to demonstrate the security, flexibility and efficiency of our approach.

Boniface Hicks, Sandra Rueda, Luke St. Clair, Trent Jaeger, and Patrick McDaniel. A logical specification and analysis for SELinux MLS policy. In Proceedings of the ACM Symposium on Access Control Models and Technologies (SACMAT), Antipolis, France, June 2007. [ bib | http | .pdf ]

The SELinux mandatory access control (MAC) policy has recently added a multi-level security (MLS) model which is able to express a fine granularity of control over a subject's access rights. The problem is that the richness of this policy makes it impractical to verify, by hand, that a given policy has certain important information flow properties or is compliant with another policy. To address this, we have modeled the SELinux MLS policy using a logical specification and implemented that specification in the Prolog language. Furthermore, we have developed some analyses for testing the properties of a given policy as well an algorithm to determine whether one policy is compliant with another. We have implemented these analyses in Prolog and compiled our implementation into a tool for SELinux MLS policy analysis, called . Using , we verified some important properties of the SELinux MLS reference policy, namely that it satisfies the simple security condition and -property defined by Bell and LaPadula

Boniface Hicks, Timothy Misiak, and Patrick McDaniel. Channels: Runtime system infrastructure for security-typed languages. In 23rd Annual Computer Security Applications Conference (ACSAC), Miami, Fl, December 2007. [ bib | http | .pdf ]

Security-typed languages (STLs) are powerful tools for provably implementing policy in applications. The programmer maps policy onto programs by annotating types with information flow labels, and the STL compiler guarantees that data always obeys its label as it flows within an application. As data flows into or out of an application, however, a runtime system is needed to mediate between the information flow world within the application and the non-information flow world of the operating system. In the few existing STL applications, this problem has been handled in ad hoc ways that hindered software engineering and security analysis. In this paper, we present a principled approach to STL runtime system development along with policy infrastructure and class abstractions for the STL, Jif, that implement these principles. We demonstrate the effectiveness of our approach by using our infrastructure to develop a firewall application, FlowWall, that provably enforces its policy.

Patrick Traynor, Mike Chien, Scott Weaver, Boniface Hicks, and Patrick McDaniel. Non-invasive host certification. In Second IEEE Communications Society/CreateNet International Conference on Security and Privacy in Communication Networks (SecureComm '06), Baltimore, MD, Aug. 28 - Sep. 1 2006. [ bib | .pdf ]

Determining whether a user or system is exercising appropriate security practices is difficult in any context. Such difficulties are particularly pronounced when uncontrolled or unknown platforms join public networks. Commonly practiced techniques used to vet these hosts, such as system scans, have the potential to infringe upon the privacy of users. In this paper, we show that it is possible for clients to prove both the pres- ence and proper functioning of security infrastructure without allowing unrestricted access to their system. We demonstrate this approach, specifically applied to anti-virus security, by requiring clients seeking admission to a network to positively identify the presence or absence of malcode in a series of puzzles. The implementation of this mechanism and its application to real networks are also explored. In so doing, we demonstrate that it is not necessary for an administrator to be invasive to determine whether a client implements good security practices.

Keywords: Certification, Assurance, Network Security, Malware are totally appropriate and are likely to be observed more Certification, Assurance, Network Security, Malware

Boniface Hicks, Kiyan Ahmadizadeh, and Patrick McDaniel. Understanding practical application development in security-typed languages. In 22st Annual Computer Security Applications Conference (ACSAC), Miami, Fl, December 2006. Awarded best student paper. [ bib | .pdf ]

Security-typed languages are an evolving tool for implementing systems with provable security guarantees. However, to date, these tools have only been used to build simple toy programs. As described in this paper, we have developed the first real-world, security-typed application: a secure email system written in the Java language variant Jif. Real-world policies are mapped onto the information flows controlled by the language primitives, and we consider the process and tractability of broadly enforcing security policy in commodity applications. We find that while the language provided the rudimentary tools to achieve low-level security goals, additional tools, services, and language extensions were necessary to formulate and enforce application policy. We detail the design and use of these tools. We also show how the strong guarantees of Jif in conjunction with our policy tools can be used to evaluate security. This work serves as a starting point-we have demonstrated that it is possible to implement real-world systems and policy using security-typed languages. However, further investigation of the developer tools and supporting policy infrastructure is necessary before they can fulfill their considerable promise of enabling more secure systems.

Boniface Hicks, Dave King, Patrick McDaniel, and Michael Hicks. Trusted declassification: High-level policy for a security-typed language. In Proceedings of the 1st ACM SIGPLAN Workshop on Programming Languages and Analysis for Security (PLAS '06), Ottawa, Canada, June 10 2006. ACM Press. An extended version of this paper appears in the technical report NAS-TR-0033-2006. [ bib | .pdf ]

Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of nonin- terference which ensures that high-security data will not be observ- able on low-security channels. Because noninterference is typically too strong a property, most programs use some form of declassifi- cation to selectively leak high security information, e.g. when per- forming a password check or data encryption. Unfortunately, such a declassification is often expressed as an operation within a given program, rather than as part of a global policy, making reasoning about the security implications of a policy more difficult.
In this paper, we propose a simple idea we call trusted declas- sification in which special declassifier functions are specified as part of the global policy. In particular, individual principals declar- atively specify which declassifiers they trust so that all informa- tion flows implied by the policy can be reasoned about in absence of a particular program. We formalize our approach for a Java- like language and prove a modified form of noninterference which we call noninterference modulo trusted methods. We have imple- mented our approach as an extension to Jif and provide some of our experience using it to build a secure e-mail client.

Moreno Falaschi, Patrick Hicks, and William H. Winsborough. Demand transformation analysis for concurrent constraint programs. In Joint International Conference and Symposium on Logic Programming, pages 333-347, 1996. An extended version of this paper appears in the Journal of Logic Programming, Vol 41, No. 3, pp 185-215. [ bib | .html ]

This paper presents a demand transformation analysis that maps a predicate's output demands to its input demands. This backward dataflow analysis for concurrent constraint programs is constructed in the framework of abstract interpretation. In the context of stream parallelism, this analysis identifies an amount of input data for which predicate execution can safely wait without danger of introducing deadlock. We assume that programs are well-moded and prove that our analysis is safe. We have constructed an implementation of this analysis and tested it on some small, illustrative programs and have determined that it gives useful results in practice. We identify several applications of the analysis results to distributed implementations of concurrent constraint languages, including thread construction and communication granularity. This analysis will enable exisiting computation cost estimation analyses to be applied to stream-parallel logic languages.

John Hannan and Patrick Hicks. Higher-order uncurrying. In Proceedings of the 25th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1-10, San Diego, CA, January 1998. An extended version of this paper appears in Higher Order and Symbolic Computation, Vol 13, No. 3, 2000, pp 179-216. [ bib | .pdf ]

We present a formal specification of unCurrying for a higher-order, functional language with ML-style let-polymorphism. This specification supports the general unCurrying of functions, even for functions that are passed as arguments or returned as values. The specification also supports partial unCurrying of any consecutive parameters of a function, rather than only unCurrying all of a function's parameters. We present the specification as a deductive system that axiomatizes a judgment relating a source term with an unCurried form of the term. We prove that this system relates only typable terms and that it is correct with respect to an operational semantics. We define a practical algorithm, based on algorithm W, that implements unCurrying and prove this algorithm sound and complete with respect to the deductive system. This algorithm generates maximally unCurried forms of source terms. These results provide a declarative framework for reasoning about unCurrying and support a richer form of unCurrying than is currently found in compilers for functional languages.

John Hannan and Patrick Hicks. Higher-order arity raising. In Proceedings of 3rd ACM SIGPLAN International Conference on Functional Programming, pages 27-38, Baltimore, MD, September 1998. [ bib | .pdf ]

Arity raising, also known as variable splitting or flattening, is the program optimization which transforms a function of one argument into a function of several arguments by decomposing the structure of the original one argument into individual components in that structure. This optimization eliminates the need for the structuring of the components and also allows more arguments to be passed in registers during a function call. We present a formal specification of arity raising for a higher-order functional language. This specification supports the general arity raising of functions, even for functions which are passed as arguments or returned as values. We define a practical algorithm, based on algorithm W, which implements arity raising, and we prove this algorithm sound with respect to the deductive system. These results provide a declarative framework for reasoning about arity raising and support a richer form of the transformation than is currently found in compilers for functional languages.

Patrick Hicks, Matthew Walnock, and Robert Michael Owens. Analysis of power consumption in memory hierarchies. In Proceedings of the 1997 international symposium on Low power electronics and design, pages 239-242. ACM Press, 1997. [ bib | DOI | .pdf ]

In this paper, we note and analyze a key trade-off: as the complexity of caches increases (higher set-associativity, larger block size, and larger overall size), the power consumed by a cache access increases. However, because the hit rate also increases, the number of main memory accesses decreases and thus the power consumed by a memory access decreases. Recent papers which consider the power consumption of caches tend to ignore hit rates. This is unfortunate, because it is undesirable to have energy-efficient caches which are also very slow. Hit rates also play a key role in truly evaluating the energy efficiency of a cache, because low hit rates lead to more frequent main memory accesses which consume more power than cache accesses.

Michael Hicks, Stephen Tse, Boniface Hicks, and Steve Zdancewic. Dynamic updating of information-flow policies. In Proceedings of the Foundations of Computer Security Workshop (FCS '05), March 2005. [ bib | .pdf ]

Applications that manipulate sensitive information should ensure end-to-end security by satisfying two properties: sound execution and some form of noninterference. By the former, we mean the program should always perform actions in keeping with its current policy, and by the latter we mean that these actions should never cause high-security information to be visible to a low-security observer. Over the last decade, securitytyped languages have been developed that exhibit these properties, increasingly improving so as to model important features of real programs. No current security-typed language, however, permits general changes to security policies in use by running programs. This paper presents a simple information flow type system for that allows for dynamic security policy updates while ensuring sound execution and a relaxed form of noninterference we term noninterference between updates. We see this work as an important step toward using language-based techniques to ensure end-to-end security for realistic applications.

Tech Reports

Boniface Hicks. Secure systems development using security-typed languages. Technical report, Penn State, University Park, PA, December 2007. [ bib | .html | .pdf ]

Boniface Hicks, Sandra Rueda, Luke St. Clair, Trent Jaeger, and Patrick McDaniel. A logical specification and analysis for SELinux MLS policy. Technical Report NAS-TR-0058-2007, Networking and Security Research Center, Department of Computer Science, Pennsylvania State University, 2007. Slightly extended version of SACMAT 2007 publication. [ bib ]

Boniface Hicks, Sandra Rueda, Trent Jaeger, and Patrick McDaniel. Breaking Down the Walls of Mutual Distrust: Security-typed Email Using Labeled IPsec. Technical Report NAS-TR-0049-2006, Network and Security Research Center, Department of Computer Science and Engineering, Pennsylvania State University, University Park, PA, USA, September 2006. [ bib ]

Recent advances in security-typed languages and operating system MAC policy have led to a renaissance in information flow security. Grounded in classical security analysis, these technologies provide guarantees preventing data of differing security levels from leaking (confidentiality) or corrupting (integrity) data from other levels. However, these works have largely advanced in isolation. In this paper we investigate the feasibility, design, and cost of unifying the information flow infrastructure at the application, operating system, and network layers. In particular, we develop an infrastructure that enforces a single consistent policy using the information flow controls of the Jif programming language (application), SELinux operating system (OS), and Labeled IPsec (network). We evaluate the security, performance, and complexity of use of the resulting system, and conclude with notes on future directions in the use of these systems. The evaluations and experiments show not only that the overheads are nominal, but that activities such as instrumenting new applications are significantly less cumbersome than in isolated information flow development.

Boniface Hicks, Dave King, Patrick McDaniel, and Michael Hicks. Trusted declassification: High-level policy for a security-typed language. Technical Report NAS-TR-0033-2006, Networking and Security Research Center, Department of Computer Science, Pennsylvania State University, March 2006. [ bib | .pdf ]

Security-typed languages promise to be a powerful tool with which provably secure software applications may be developed. Programs written in these languages enforce a strong, global policy of noninterference for all their data. Unfortunately, real programs almost always require the use of noninterference-violating flows introduced by declassification. This causes the global policy to break down and obscures the meaning of security labels. These languages suffer from the lack of an alternative, global policy which can handle declassifications. In this paper, we present a security-typed, object-oriented language which allows trusted declassifications based on a global policy. We prove the soundness of our language as well as a modified form of noninterference, which we call noninterference modulo trusted declassification. We implement our declassification mechanism and global security policy in Jif and provide some examples which motivate its use.

Boniface Hicks, Dave King, and Patrick McDaniel. Declassification with Cryptographic Functions in a Security-Typed Language. Technical Report NAS-TR-0004-2005, Network and Security Center, Department of Computer Science, Pennsylvania State University, January 2005. (updated May 2005). [ bib | .pdf ]

Security-typed languages are powerful tools for provably enforcing noninterference. Real computing systems, however, often intentionally violate noninterference by deliberately releasing (or declassifying) sensitive information. These systems frequently trust cryptographic functions to achieve declassification while still maintaining confidentiality. We introduce the notion of trusted functions that implicitly act as declassifiers within a security-typed language. Proofs of the new language's soundness and its enforcement of a weakened form of noninterference are given. Additionally, we implement trusted functions used for declassification in the Jif language. This represents a step forward in making security-typed languages more practical for use in real systems.

Boniface Hicks, Patrick McDaniel, and Ali Hurson. Information flow control in database security: A case study for secure programming with jif. Technical Report NAS-TR-0011-2005, Network and Security Center, Department of Computer Science, Pennsylvania State University, April 2005. [ bib | .pdf ]

Because of the increasing demands for privacy and integrity guarantees in applications that handle sensitive, electronic data, there is a need for automated software development tools and techniques for enforcing this security. Although there have been many attempts to apply security to existing systems after the fact, manifold failures indicate that this approach should be revisited. To the contrary, experience indicates that secure systems must be designed with explicit policies from the beginning and that there should be some automated, mathematically-verifiable mechanism to aid programmers in doing this correctly. Recent research in language-based security has made great strides towards the development of sophisticated and robust languages for programming with explicit security policies. Insufficient experience with these languages, however, has left them untested and impractical for writing real, distributed applications. In this paper, we present our experiences of working with Jif, a Java-based, security-typed language, in building a distributed, database application. Our experience has indicated the current impracticality of programming in Jif, but has helped us to identify language development tools and automation algorithms that could aid in making Jif more practical for developing real, distributed applications.