Christian Skalka, Publications

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher order programs. The properties verified are based on the ordered sequence of events that occur during program execution, so called event traces. Our type and effect systems infer conservative approximations of the event traces arising at run-time, and model-checking techniques are used to verify logical properties of these histories. Our language model is based on the lambda-calculus. Technical results include a type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the trace effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms. A type safety result is proven for both unification and subtyping constraint versions of the type system, ensuring that statically well-typed programs do not contain trace event checks that can fail at run-time.

We develop a static analysis which distills first-order computational structure from higher-order functional programs. The analysis condenses higher-order programs into a first-order rule-based system, a nugget, that characterizes all value bindings that may arise from program execution. Theorem provers are limited in their ability to automatically reason about higher-order programs; nuggets address this problem, being inductively defined structures that can be simply and directly encoded in a theorem prover. The theorem prover can then prove non-trivial program properties, such as the range of values assignable to particular variables at runtime. Our analysis is flow- and path-sensitive, and incorporates a novel prune-rerun analysis technique to approximate higher-order recursive computations.

The Java JDK security model provides an access control mechanism for the JVM based on dynamic stack inspection. Previous results have shown how stack inspection can be enforced at compile time via whole-program type analysis, but features of the JVM present significant remaining technical challenges. For instance, dynamic dispatch at the bytecode level requires special consideration to ensure flexibility in typing. Even more problematic is dynamic class loading and linking, which disallow a purely static analysis in principle, though the intended applications of the JDK exploit these features. We propose an extension to existing bytecode verification, that enforces stack inspection at link time, without imposing new restrictions on the JVM class loading and linking mechanism. Our solution is more flexible than existing type based approaches, and establishes a formal type safety result for bytecode-level access control in the presence of dynamic class linking.

Trust management systems are frameworks for authorization in modern distributed systems, allowing remotely accessible resources to be protected by providers. By allowing providers to specify policy, and access requesters to possess certain access rights, trust management automates the process of determining whether access should be allowed on the basis of policy, rights, and an authorization semantics. In this paper we survey modern state-of-the-art in trust management, focusing on features of policy and rights languages that provide the necessary expressiveness for modern practice. We characterize systems in light of a generic structure that takes into account components of practical implementations. We emphasize systems that have a formal foundation, since security properties of them can be rigorously guaranteed. Underlying formalisms are reviewed to provide necessary background.

Distributed authorization takes into account several elements, including certificates that may be provided by non-local actors. While most trust management systems treat all assertions as equally valid up to certificate authentication, realistic considerations may associate risk with some of these elements, for example some actors may be less trusted than others. Furthermore, practical online authorization may require certain levels of risk to be tolerated. In this paper, we introduce a trust management logic that incorporates formal risk assessment. This formalization allows risk levels to be associated with authorization elements, and promotes development of a distributed authorization algorithm allowing tolerable levels of risk to be precisely specified and rigorously enforced.

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features. We also extend the basic language model with exceptions and stack-based event contexts, and show how trace effects scale to these extensions by structural transformations.

We propose the monadic linear logic programming language LolliMon as a new foundation for the specification of distributed trust management systems, particularly the RT framework. LolliMon possesses features that make it well-suited to this application, including rigorous logical foundations, an expressive formula language, strong typing, and saturation as a proof resolution strategy. We specify certificate chain discovery in full RT for authorization in a distributed environment where certificates may be stored non-locally and selective retrieval is necessary. The uniform LolliMon specification of authorization and certificate chain discovery eases formal reasoning about the system, and scales to a rich collection of trust management features. The executable LolliMon specification also serves as a prototype implementation.

Through web service technology, distributed applications can be built in an open and flexible manner, bringing tremendous power to applications on the web. However, this flexibility poses significant challenges to security. Traditional access control for distributed systems is not flexible and efficient enough in such an environment; in particular, fully secure online authorization decisions may be too inefficient in practice, requiring simplifications which may have only an informal and unverifiable relation to fully secure authorization decisions. This paper introduces a trust-but-verify framework for web services authorization. In this framework, each web service maintains the usual access control policies, as well as a ``trust transformation'' policy, that formally specifies how to simplify full authorization into a more efficient form for online checking. This formalization allows certainty that offline checking verifies the trust relation between full security and online checking.

Distributed authorization takes into account several elements, including certificates that may be provided by non-local actors. While most trust management systems treat all assertions as equally valid up to certificate authentication, realistic considerations may associate risk with some of these elements; some actors may be less trusted than others, some elements may be more computationally expensive to obtain, and so forth. Furthermore, practical online authorization may require certain levels of risk to be tolerated. In this paper, we introduce a trust management logic that incorporates formal risk assessment. This formalization allows risk levels to be associated with authorization elements, and promotes development of a distributed authorization algorithm allowing tolerable levels of risk to be precisely specified and rigorously enforced.

Trace effects are statically generated program abstractions, that can be model checked for verification of assertions in a temporal program logic. In this paper we develop a type and effect analysis for obtaining trace effects of Object Oriented programs in Featherweight Java. We observe that the analysis is significantly complicated by the interaction of trace behavior with inheritance and other Object Oriented features, particularly overridden methods, dynamic dispatch, and downcasting. We propose an expressive type and effect inference algorithm combining polymorphism and subtyping/subeffecting constraints to obtain a flexible trace effect analysis in this setting, and show how these techniques are applicable to Object Oriented features.

This paper describes a flexible type and effect inference system for Featherweight Java (FJ). The effect terms generated by static type and effect inference embody the abstract interpretation of program event sequences. Flexibility in the analysis is obtained by post-processing of inferred effects, allowing a modular adaptation to extensions of the language. Several example transformations are discussed, including how inferred effects can be transformed to reflect the impact of exceptions on FJ control flow.

The Java Security Architecture includes a dynamic mechanism for enforcing access control checks, the so-called stack inspection process. While the architecture has several appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. This paper develops type systems which can statically guarantee the success of these checks. Our systems allow security properties of programs to be clearly expressed within the types themselves, which thus serve as static declarations of the security policy. We develop these systems using a systematic methodology: we show that the security-passing style translation, proposed by Wallach, Appel and Felten as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems.

The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A use-based approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type safety result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.

Through web service technology, distributed applications can be built in a flexible manner, bringing tremendous power to applications on the web. However, this flexibility poses significant challenges to security. In particular, an end user (be it human or machine) may access a web service directly, or through a number of intermediaries, while these intermediaries may be formed on the fly for a particular task. Traditional access control for distributed systems is not flexible and efficient enough in such an environment. Indeed, it may be impossible for a web service to anticipate all possible access patterns, hence to define an appropriate access control list beforehand. Novel solutions are needed.

This paper introduces a trust-but-verify framework for web services authorization, and provides an implementation example. In the trust-but-verify framework, each web service maintains authorization policies. In addition, there is a global set of ``trust transformation'' rules, each of which has an associated transformation condition. These trust transformation rules convert complicated access patterns into simpler ones, and the transformation is done by a requester (the original requester or an intermediary) with the assumption that the requester can be trusted to correctly omit certain details. To verify authorization, the requester is required to document evidence that the associated transformation conditions are satisfied. Such evidence and support information can either be checked before access is granted, or can be verified after the fact in an offline mode, possibly by an independent third party.

This paper shows how type effect systems can be combined with model-checking techniques to produce powerful, automatically verifiable program logics for higher-order programs. The properties verified are based on the ordered sequence of events that occur during program execution-an event history. Our type and effect systems automatically infer conservative approximations of the event histories arising at run-time, and model-checking techniques are used to verify logical properties of these histories.

Our language model is based on the lambda-calculus. Technical results include a powerful type inference algorithm for a polymorphic type effect system, and a method for applying known model-checking techniques to the history effects inferred by the type inference algorithm, allowing static enforcement of history- and stack-based security mechanisms.

We present pml_B, a programming language that includes primitive sets and associated operations. The language is equipped with a precise type discipline that statically captures dynamic properties of sets, allowing runtime optimizations. We demonstrate the utility of pml_B by showing how it can serve as a practical implementation language for higher-level programming language based security systems, and characterize pml_B by comparing the expressiveness of pml_B sets with enumerations.

The HM(X) framework is a constraint-based type framework with built-in let-polymorphism. This paper establishes purely syntactic type soundness for the framework, treating an extended version of the language containing state and recursive binding. These results demonstrate that any instance of HM(X), comprising a specialized constraint system and possibly additional functional constants and their types, enjoys syntactic type soundness.

The confinement of object references is a significant security concern for modern programming languages. We define a language that serves as a uniform model for a variety of confined object reference systems. A use-based approach to confinement is adopted, which we argue is more expressive than previous communication-based approaches. We then develop a readable, expressive type system for static analysis of the language, along with a type safety result demonstrating that run-time checks can be eliminated. The language and type system thus serve as a reliable, declarative and efficient foundation for secure capability-based programming and object confinement.

The Java JDK 1.2 Security Architecture includes a dynamic mechanism for enforcing access control checks, so-called stack inspection. This paper studies type systems which can statically guarantee the success of these checks. We develop these systems using a new, systematic methodology: we show that the security-passing style translation, proposed by Wallach and Felten as a dynamic implementation technique, also gives rise to static security-aware type systems, by composition with conventional type systems. To define the latter, we use the general HM(X) framework, and easily construct several constraint- and unification-based type systems. They offer significant improvements on a previous type system for JDK access control, both in terms of expressiveness and in terms of readability of type specifications.

A number of security systems for programming languages have recently appeared, including systems for enforcing some form of access control. The Java JDK 1.2 security architecture is one such system that is widely studied and used. While the architecture has many appealing features, access control checks are all implemented via dynamic method calls. This is a highly non-declarative form of specification which is hard to read, and which leads to additional run-time overhead. In this paper, we present a novel security type system that enforces the same security guarantees as Java Stack Inspection, but via a static type system with no additional run-time checks. The system allows security properties of programs to be clearly expressed within the types themselves. We also define and prove correct an inference algorithm for security types, meaning that the system has the potential to be layered on top of the existing Java architecture, without requiring new syntax.

The Actor Specification Diagram Language is a rigorously defined graphical specification language, with features for modelling concurrency and asynchronous communication. These features make the language appropriate for the formal analysis of distributed security protocols. The graphical nature of the language makes protocol descriptions easy to read and understand, vital properties for appeal to a wider user population. Proofs of protocol correctness can be given via graphical transformation, with each step of transformation justified by rigorous argument if desired. To illustrate the utility of a graphical specification language we analyze the well-known Needham-Schroeder Pubic Key protocol.

Programming language-based security provides applications programmers with greater control and flexibility for specifying and enforcing security policies. As computing environments distribute and diversify, and demands for program mobility increase, this power allows programmers to adapt software to developing needs, while still protecting resources. This thesis advocates the use of static type disciplines for expressing and enforcing programming language-based security. We develop type systems for two popular security models: the Access Control model with Stack Inspection, and the Object Confinement model. Type safety proofs demonstrate that these type systems reliably enforce security statically, and imply that certain run-time optimizations may be effected for programs. The declarative nature of our type terms also provide programmers with useful and understandable descriptions of security properties. To formally develop these type systems, a transformational approach is used, where source languages are embedded in a target language, containing sets of atomic elements and associated operations, which is pre-equipped with a sound type system. This target language and type system is developed using the type constraint framework HM(X). The transformational approach and HM(X) both allow the re-use of existing theory and implementations, easing proof effort, inspiring design, and providing greater confidence in the correctness of results.

The ML datasort declaration is an extension to Standard ML allowing the declaration of refinement types, which correspond to subsets of pre-existing ML datatypes. Refinement types provide the programmer with a more precise method of expressing data structure, can prevent the occurence of certain run -time exceptions, and assist in the expression and maintenance of some representation invariants. ML refinement types correspond to regular term and regular tree languages, except that refinement types are polymorphic. While algorithms have been defined which determine the emptiness, intersection and subset problems for regular terms, the corresponding problems for polymorphic regular terms have not been studied. This thesis formally describes a refinement type language, and defines algorithms relevant to these decision problems, which are proven correct. Along with theoretical interest, these algorithms have practical applications for refinement type checking.