Manifest Security for Distributed Information
Karl Crary Robert Harper Frank Pfenning
Carnegie Mellon University
Benjamin C.Pierce Stephanie Weirich Stephan Zdancewic
University of Pennsylvania
March6,2006
Project Summary
What is the best way to build programs that compute with data sources controlled by multiple prin-cipals,while ensuring compliance with the curity policies of the principals involved?The objective of this project is to devi methods for building manifestly cure applications for an information grid consisting of multiple data sources controlled by multiple principals.This is achieved by using techniques from mathematical logic,programming language mantics,and mechanized reasoning to ensure curity of application code,while permitting convenient expression of complex computations wi
th data sources on the information grid.The project will design and implement a programming language who type system ensures compliance with curity policies through the u of proofs in a formal logic of authorization during both the static and dynamic phas of processing.The project will u automated reasoning tools such as theorem provers and logical frameworks to prove formally and rigorously the curity properties of the programming language.As a result,every application written in the language enjoys the guarantees afforded by the language as a whole.
The intellectual merit of the project consists of scientific and engineering techniques for build-ing practical programs for computing with multiple data sources that are manifestly cure.Manifest curity means that the trust relationships,access control and informationflow policies,and proofs of compliance with the policies are made manifest in the framework through the u of formal logical methods for specifying and verifying them.The properties will be formally verified against preci specifications written in a novel logic of authorization and informationflow using mechanized theorem provers and logical frameworks so that there is a direct link between the theoretical analysis and the executable code.This ensures that running applications are manifestly in compliance with the curity policies of the principals on the information grid to an extent not previously achievable in practical systems.The project will build a cure information grid and associated applications to dem
死兆星锤石
onstrate the effectiveness of its approach and provide a means for comparison with competing methods.
The broader impacts of the project include the development of fundamental technology to ensure privacy while permittingflexible access to disparate,and independently controlled,data sources.Making curity policies themlves,and proofs of application compliance with them,read-ily available in machine-checkable form is a technical cornerstone for ensuring privacy without unduly limiting the legitimate u of the data sources.The project will also significantly increa collab-oration between two major rearch universities within the Commonwealth of Pennsylvania.The participants have an established record of fostering education in thefield through writing textbooks, developing new class and cour materials at their universities,and organizing summer schools for students throughout the world.The project will also employ undergraduate rearchers through direct funding and the NSF Rearch Experience for Undergraduates program.Both participating departments have vibrant organizations supporting and promoting women in computer science,and we will work toward involving women in our project at both undergraduate and graduate level.
Project Description
1Overview
Managers of information repositories today face a tension between curity and accessibility of the information they control.Ideally,a manager wishes to make some t of information readily and conveniently accessible for legitimate us,while still ensuring that no information is leaked or modified inappropriately or without authorization.However,prent-day solutions provide good facilities only for one side or the other.On the curity side,it is fairly well understood how to prevent unauthorized leakage or modification of information by limiting data access to properly privileged queries.This works well provided the gatekeeping and authentication protocols are sound and correctly implemented.Yet,even when all works correctly,access is typically limited to a pre-specified t of queries.Moreover,since protocols and implementations often are not correct,it makes good n to protect particularly nsitive information by keeping it offthe network entirely. On the accessibility side,there has been considerable progress in the grid computing community on the problem of mobile code,wherein programs are able to move across the network to their data of interest and freely compute with it there[28].This paradigm allows for considerableflexibility in the exploitation of information,becau participants may supply their own code to be run by other sites. However,such projects have typically assumed that all participants trust each other.What curity is provided focus mainly on authentication and simple access control,providing no assurance that the accesd information is ud appropriately.Rearch on certified code[70,61,95,22]has sought t
o weaken the assumptions of mutual trust.However,the work in certified code has focud on preventing mobile code from attacking its host or bypassing its host’s access controls,not on complex reasoning about authorization or controlling the propagation of information.This tension between curity and accessibility,together with the added problem of correctness,has led to an unsatisfying state of affairs.Information is either(1)accessible but incure,(2)believed to be cure but not very accessible,or(3)definitely cure but completely off-line.
We propo to develop the theoretical and engineering basis for a cure information grid.In our propod framework,code will be free to move throughout the grid,but before such code may be executed,it must establish to its host that it complies with the host’s policy regarding u and propagation of its data.
迅雷成吉思汗美女的屁股Architecture The overall architecture of an information grid is shown in Figure1.There are veral key components to an information grid.First,we have a rich policy language,expressive enough to specify both authorization and information-flow policies.Together,the policies regulate the u and propagation of information throughout the system.The policy language is ud at all stages of grid software lifecycle:During development,it is ud to express constraints on legal program behaviors that can be checked statically.During deployment,policies appearing in code certificates are verified
by hosts to ensure compliance with their own local data polices.Finally, during execution of grid software,the policy language provides the vocabulary for authorization checks that are performed at run time to enforce access control.The policy language(described in more detail below)is bad on an open-ended authorization logic.
Next,we have a programming language and accompanying certifying compiler The programming language employs a strong type system that us the policy language for specification of information-flow and authorization policies.The programming language also provides features for describing the locality of data sources and the curity policies that govern them.The certifying compiler receives two inputs:the program,including its confidentiality and integrity policy annotations,plus information about the trust relationships between principals and hosts in the information grid.This grid information is again expresd as a collection of statements in the policy language.The compiler produces,in addition to executable output,a mechanically verifiable certificate witnessing the type safety of the resulting object code.
Finally,the runtime system provides three rvices to grid software.First,it checks the certificate accompanying any code it is asked to execute—this protects the host against malicious or corrupted code by ruling out potentialflaws(like buffer overflows,etc.)and ensures that the code complies with
the host’s local information-flow policy.This part of the curity enforcement occurs before the code is run;the certificate verifier is part of the trusted computing ba.Second,the runtime manages digital certificates that reprent proof witness for the authorization checks the code needs to make as the software is running.And third,the runtime provides cure inter-host communication:when, during the cour of execution,a grid program needs to exchange data with or nd code to another host in the grid,it does so through the runtime system,which applies appropriat
e authentication and encryption to ensure that the underlying communication channel is cure.
Manifest Security The unifying theme of the information grid architecture is manifest curity: all the steps in the chain of reasoning showing that a given program may safely be executed by a given host—including both curity policies(including trust relationships among principals and hosts)and the arguments showing that the program obeys them—are made explicit with concrete evidence in the form of machine-checkable proofs.
Manifest curity has a number of appealing advantages.Making the type safety and policy compliance of the executable code manifest protects the hosts of the grid from malicious attack. Manifest curity also facilitates auditing the behavior of the system.At runtime,explicitly con-structed proofs of authorization decisions make it possible to account for the behavior of the system and,when things go wrong(hosts crashing,passwords or keys being compromid,etc.),identify and localize the problem.Statically,making the policies manifest means that it is possible to check them for consistency and to identify assumptions.Mechanical verification of the properties leads to high degree of confidence in the system’s correctness.
国庆节法定假日几天In practice,the only scalable way to construct evidence of compliance for a large number of grid prog
rams is to begin by verifying,once and for all,the curity properties of the programming lan-guage in which the programs are written:the type safety of the language as a whole then establishes that any given program complies with its stated policy as long as it is well typed.Conquently, the type safety of the source language is of critical importance,and,following the idea of mani-fest curity,it must also be made explicit in a mechanically verifiable way.Thus,a key aspect of the information grid is the mechanical verification of the metatheoretic properties(type safety, noninterference,etc.)of the programming language and accompanying infrastructure.
To summarize,the central idea of the propod work is making the curity of the information grid infrastructure manifest.The soundness of the language is made manifest by a proof carried out explicitly in a formalized metalogic.The fact that a particular executable program accords with the
type system of the language is made manifest through the process of typechecking and certifying compilation.Which hosts are allowed to manipulate which data is made manifest by policies that explicitly describe the trust relationships among hosts and principals in the grid.The authorization decisions made by an executing program are made manifest by requiring the system to be able to dynamically produce certificates that correspond to proofs in the authorization logic.And the policies themlves are made manifest as formal objects referred to by the proofs.The upshot of all of this
is that we obtain strong assurance that the programming language and compiler are sound, that the curity policies ud in a system are consistent and consistently enforced,and that any informationflows or access control decisions made by the running system comply with the policy. An Example One of the applications we intend to build to stress-test our infrastructure is an information grid for managing journal paper submissions and reviewing.(We will focus on curity and information management issues:implementing a full-blown journal management system with a sophisticated web-browr interface,etc.,is beyond the scope of the project.)The application will support multiple journals,with some level of trust but not complete sharing of information among the principals associated with the different journals(for example,each journal will want to keep its reviews and the identity of its reviewers cret).The principals include the editor(s)for each journal,the reviewers,the authors,and the general public.This domain offers many opportunities for formalization of interesting authorization and crecy policies.(For example,assigned referees can read the paper(s)to which they are assigned,but no others,and only once they are assigned and have agreed;they can submit a report but cannot revi it on their own;they can e other reports [in anonymous form]once a decision is reached,or earlier if the editor authorizes it;accepted papers can be viewed by the general public;etc.)As a more interesting twist,we also allow the journal editors to share information about reviewers:we introduce another principal called the“reviewer clearinghou,”
who job it is to maintain a databa of reviewers,with their affiliations,areas of experti,etc.,that can be queried by journal editors.Moreover,the databa includes performance information such as average completion times for reviews and“helpfulness scores”assigned by editors of papers for which they have written reviews.Similar features are already implemented in widely deployed journal management systems;their obvious delicacy and potential for abu make them a perfect ca study for an infrastructure like ours,where ownership of information is decentralized and where policies and their verification are both made manifest.
One concrete way of getting relevant information from the journals into the reviewer clearinghou databa is for the implementor of the clearinghou to write a snippet of code that is distributed to the hosts responsible for each of the journals,to be run whenever a new review is entered(or another event of interest takes place)so that appropriate information can be nt back in the form of a small mobile agent that moves back to the clearinghou and updates its databa.The“curity lifecycle”of one of the code snippets is as follows:It is written and compiled on the clearinghou host,which,during typechecking,verifies its compliance with the policies published by the journal hosts and produces a certificate demonstrating that the object code produced by the compiler is indeed compliant.This certificate is transmitted along with the object code to the journal hosts, which
themlves verify the validity of the certificate with respect to the code,before installing it in some internal list of event handlers.Alternatively,the clearinghou itlf might initiate the execution of a similar snippet,nding agents to each of the journals to gather and carry back data in compliance with their policies.Both alternatives involve the notion of a“located computation,”which takes place in a specified curity context and which can move,consistently with policy,from one such context to another.
Assumptions,Limitations,and Non-Goals With any propod technique for enforcing curity policies,it is necessary to make some assumptions about the context in which the system will be deployed—the same is true of an information grid.The assumptions help to delimit the scope and provide traction on the issues at the heart of the project.The work we propo here is largely focud on protecting hosts from potentially malicious code and preventing malicious hosts from disrupting global confidentiality and authorization constraints.Our project will also build on existing results and standard techniques(such as the u of public-key cryptography).The primary assumptions, limitations,and explicit non-goals of our project are as follows.
gcc命令
First,we assume an underlying infrastructure suitable for reliably exchanging code and data among the hosts of the grid(for example,as provided by the standard TCP/IP protocols).Hosts participating i
n an information grid,and,in particular,their runtime systems,may be trusted to varying degrees by the principals involved in the system(the trust relationships are specified by explicit policies);the network is not trusted.
Second,we employ standard cryptographic techniques to ensure confidential and authenticated communication between hosts in the network.For the purpos of our mechanical verification,we make the standard Dolev-Yao assumptions[27]and treat encryption operations as perfect.
Third,for the sake of practicality and tractability,some parts of the implementation behavior won’t be modeled.For example,low-level details about caching and timing effects will be omitted, and we will assume that it is intractable for the attacker to perform complete network traffic analysis. Conquently,there is the possibility that an attacker able to interact with the information grid at level of abstraction lower than the one we model may be able to circumvent its information-flow policies.Such abstraction-violation attacks are always possible,regardless of where the abstraction boundary is drawn.Existing work on preventing low-level timing[5]and network traffic analysis attacks could in principle be applied in our context,but we will not focus on this here.
Fourth,our work will not address the issues of fault tolerance and reliability that are typically address
ed by replication and the u of connsus protocols(although it is likely that tho techniques could be fruitfully applied in an information grid).Our propod work also does not address denial of rvice attacks—the focus of this work is on integrity of grid software and the confidentiality of data,not on availability of the system.
This list is certainly incomplete,but we believe that the philosophy of manifest curity will itlf help to identify and articulate additional assumptions and limitations that may ari.
2Propod Work
Our approach to building applications with manifestly cure access to distributed information is founded on logic,type theory,and mechanically verifiable proofs.This ction discuss in more detail the technical challenges we must face in each of the areas and our plans for addressing them.
2.1Grid Security Policies:A Logic of Authorization and Knowledge
To reason about and enforce properties of our infrastructure and of programs executing on it,we must be able to specify curity policies.Thefirst component of our propod rearch is thus the development of an appropriate policy language for authorization and informationflow.Since our goal i
s to design and implement aflexible,open-ended architecture,the specification language itlf must be both expressive and open-ended.Moreover,we wish to reason formally about properties of curity policies in order to avoid unintended conquences of policy decisions.Finally,we would like to be able to verify grid software against the curity policies.This ction sketches some underlying logical principles for the policy language and some preliminary evidence for the viability of our approach.We begin by decomposing the problem into authorization and informationflow. Authorization answers the question of which principals are permitted to access which resources. Informationflow specifies the permissible conquences of properly authorized access. Authorization policies We want a logic in which one can reason about whether a principal should have access to a resource.Logics for reasoning about access control go back to work by Abadi et al.[4,2].However,prior work does not completely satisfy our design criteria—in particular, generality and extensibility is difficult to combine with the ability to reason mechanically about policies as a whole(e the related work discussion below).
罗非鱼的做法大全
Briefly,a principal K should be granted access to a resource R exactly if there is a proof of may-access(K,R).We may understand the meaning of this proposition by considering the pertinent judgements and proof rules[31,53,78].The most basic judgment is that of the truth of a proposition, w
ritten as A true.We furthermore need a judgment of affirmation,written K affirms A,expressing a policy of K.For example,K affirms may-access(L,R)is a policy statement by principal K that
L may access resource R.This implies the truth of may-access(L,R)if K also controls the resource R.Thefinal ingredient is the standard notion of hypothetical judgment.We writeΓ=⇒A true andΓ=⇒K affirms A,whereΓis a collection of assumptions of the form B true or K affirms B.
We now sketch a quent calculus for reasoning about authorization.We begin with the so-called judgmental rules which explicate the meaning of the judgments:
Γ,P true=⇒P true
Γ=⇒A true
Thefirst rule express that from the assumption P we can obtain the conclusion P.The cond, that when A true any principal K is prepared to affirm A.Since A is true and has an explicit proof, there is no reason for K to deny it.Converly,if K affirms A,then A is true from K’s point of view—i.e.,we may assume that A is true while establishing an affirmation for the same principal K:
Γ,A true=⇒K affirms C
Γ,K affirms A=⇒K affirms C
In order to u affirmations within propositions(to form policies that require the conjunction of two affirmations,for example),the logic must internalize them as propositions.The syntax K A packages an affirmation judgment as a proposition:
体操队Γ=⇒K affirms A Γ=⇒ K A true
Γ,A true=⇒K affirms C Γ, K A true=⇒K affirms C
An authorization policy is now just a t of assumptionsΓ.An authorization query is a conclu-sion,usually of the form K affirms may-access(L,R)where K controls resource R.Principal L will be granted access if there is a proof of the query fromΓ.Our authorization architecture will follow proof-carrying authorization[9,10],wherein L supplies such a proof explicitly for validation by a resource monitor implemented in the grid runtime system.At the leaves of the proofs are digitally signed certificates that witness the policy statements of the principals as collected inΓ.
All this rais veral issues,such as how to concretely express policies and proofs,how to asm-ble proofs,and how to verify their correctness.Our grid architecture will u a logical framework[80] th
广州市儿童公园
at is explicitly designed for the reprentation of logics and proofs.This design makes the archi-tecture inherently open-ended:we can enrich our logic with further connectives while still using the same implementation.Furthermore,we can formally reason about the logic and about specific poli-cies using the meta-theoretic reasoning capabilities of the framework.This is uful to,for example, establish that a curity policy is consistent.
Information-flow policies Authorization policies govern which principals are allowed to access which resources,but they do not specify what tho principals may do with the data once they have permission to access it.Information-flow policies,in contrast,restrict the propagation and dismination of information throughout the information grid.
Suppo that principal L has been granted access tofile R(by prenting a proof of may-access(L,R) to the runtime reference monitor).What kind of informationflow does this actually entail—i.e., what knowledge can various principles now derive?
In order to define a logic of knowledge,we need a new judgment,K knows A,where A is a proposition.Clearly,if K knows A,then A should be true.Conquently,any judgement J entailed by A true is entailed by K knows A:
Γ,A true=⇒J
Γ,K knows A=⇒J
The conver is fal,and this is the very esnce of crecy:there are many true propositions that K does not(and should not)know.We establish that K knows A by showing that K can infer A using only its own knowledge.We formalize this using the restriction operatorΓ|K,which eras fromΓall hypothes not of the form K knows B.
Γ|K=⇒A true
Γ=⇒K knows A
