PSU CSE 543 - Development in Security typed Languages

Unformatted text preview:

IntroductionOverviewJPmailSecurity policyThe Jif programming languageAn overview of JPmailImplementationSecure software engineeringSecurity policyDistributed policyToolsSoftware EngineeringHigh-Level PolicyPolicy storePolicy compilerDeclassifiersDistributed PolicyEvaluationTesting JPmailTwo criteria for evaluationEffectiveness for secure programmingThe difficulty of programming in JifNeeds for improvementRelated WorkConclusionAvailabilityA brief description of JifScreen ShotsFrom Languages to Systems: Understanding Practical ApplicationDevelopment in Security-typed LanguagesBoniface Hicks, Kiyan Ahmadizadeh and Patrick McDanielSystems and Internet Infrastructure Security Laboratory (SIIS)Computer Science and Engineering, Pennsylvania State University{phicks,ahmadiza,mcdaniel}@cse.psu.eduAbstractSecurity-typed languages are an evolving tool for im-plementing systems with provable security guaran-tees. However, to date, these tools have only beenused to build simple “toy” programs. In this pa-per, we explore the process and machinery of build-ing provably secure applications using security-typedlanguages. We develop a secure email system inthe Java language variant Jif. Real world policiesare mapped onto the information flows controlled bythe language primitives, and we consider the processand tractability of broadly enforcing security policyin commodity applications. In this investigation, wefound that while the language provided the rudimen-tary tools to achieve low-level security goals, addi-tional tools, services, and language extensions werenecessary to formulate and enforce application pol-icy. We detail the design and use of these tools. Thiswork serves as a starting point–we have demonstratedthat it is possible to implement real world systems andpolicy using security-typed languages. However, fur-ther investigation of the developer tools and support-ing policy infrastructure is necessary before they canfulfill their considerable promise of enabling more se-cure systems.1 IntroductionThe exposure of private data is an increasingly criti-cal concern of online organizations [8, 9]. The hugecosts of exposure can be measured both in financialand in human terms. The central cause is, of course,the systems themselves. The security provided byexisting systems is largely due to secure design andimplementation–practices that have yet to fully ma-ture. Furthermore, the subsequent evaluation of thesesystems relies on ad hoc or inexact quality and as-surance evaluations. What are needed are tools forformulating and ensuring more precise notions of se-curity. Security-typed languages fulfill this need.Security-typed languages annotate source codewith security levels on types [33] such that the com-piler can statically guarantee that the program will en-force noninterference [14]. In a broader sense, theselanguages provide a means of provably enforcing asecurity policy. Theoretical models for security-typedlanguages have been actively studied and are con-tinuing to evolve. For example, researchers are ex-tending these models to include new features, such asexceptions, polymorphism, objects, inheritance, side-effects, threads, encryption, and many more [25].However, developer tools and programming expe-rience have not evolved in concert with language fea-tures. There are currently only two significant lan-guage implementations, Flow Caml [28] and Jif [22]and only two applications [1, 22], both written in Jif.The literature frequently postulates on practical, dis-tributed applications with many principals and com-plex policy models such as tax preparation [20], med-ical databases [30] and banking systems [31]. How-ever, the only completed applications have both been“toy” applications with only two principals within asimplistic distributed environment. For this reason,many important language features such as dynamicprincipals and declassification, as well as integrationwith conventional security mechanisms such as cryp-tography, certificates and certificate authorities are yetto be fully explored.To address this lack of practical experience, we setout to build a realistic application in a security-typedlanguage. We sought to discover whether this tool1for secure programming could hold up to its promiseof delivering real-world applications with strong se-curity guarantees. We conducted this experiment byimplementing an email system in the language Jif, asecurity-typed variant of Java. Throughout this paper,we reflect on the advantages and limitations of theselanguage-based security tools and the requirements offuture system development.A principal result of this study is that while lan-guage tools were robust and expressive, additional de-velopment and runtime tools were necessary. We ex-tend the language with additional policy formulationtools (a policy compiler [15]) and runtime support in-frastructure (policy store) to enable the enforcementof policy in a distributed environment. We also pro-vide tools for secure software engineering includinga Jif IDE in the Eclipse extensible development plat-form. Finally, we provide a critical evaluation of theJif language, highlighting its effectiveness at carry-ing out the promised security goals, the difficulties in-volved in using it and the ways in which it still needsimprovement.In a sense this paper is the second chapter in anongoing story, because we are not the first to of-fer our experience with Jif. Askarov and Sabelfeldgave the first detailed experience paper on Jif lastyear [1]. Various aspects of this work set it apartfrom theirs. These center around the fact that ourgoals were divergent—while they sought to verifythe security properties of a cryptographic protocol,we have sought to build a real, distributed, interac-tive application, which interoperates with other ex-isting applications. As a consequence of their goal,the policy used in their program is a relatively sim-ple, two-principal policy. In contrast, a significantpart of the contribution of this work lies in the toolswe have implemented for handling more complex andexpressive distributed policies. Another contributionincludes the cryptographic infrastructure we developwhich was necessitated by the distributed, real-worldnature of our application.The remainder of this paper is organized as follows.We begin in the next section by providing a sketch ofan email system and the kinds of security policies itrequires. Section 3 discusses the details of our


View Full Document

PSU CSE 543 - Development in Security typed Languages

Documents in this Course
Agenda

Agenda

14 pages

HYDRA

HYDRA

11 pages

PRIMA

PRIMA

15 pages

CLIMATE

CLIMATE

15 pages

Load more
Download Development in Security typed Languages
Our administrator received your request to download this document. We will send you the file to your email shortly.
Loading Unlocking...
Login

Join to view Development in Security typed Languages and access 3M+ class-specific study document.

or
We will never post anything without your permission.
Don't have an account?
Sign Up

Join to view Development in Security typed Languages 2 2 and access 3M+ class-specific study document.

or

By creating an account you agree to our Privacy Policy and Terms Of Use

Already a member?