%0 Conference Paper %B IEEE Symposium on Security and Privacy, 2008. SP 2008 %D 2008 %T Fable: A Language for Enforcing User-defined Security Policies %A Swamy,N. %A Corcoran,B.J. %A Hicks, Michael W. %K Access control %K Automata %K Collaborative work %K Communication system security %K Computer languages %K computer security %K Data security %K enforcement policy %K FABLE %K Government %K high-level security goals %K information flow %K Information security %K Language-based security %K programming languages %K Programming profession %K provenance %K security automata %K security labels %K security of data %K user-defined security policies %K verified enforcement %K Web programming language %X This paper presents FABLE, a core formalism for a programming language in which programmers may specify security policies and reason that these policies are properly enforced. In FABLE, security policies can be expressed by associating security labels with the data or actions they protect. Programmers define the semantics of labels in a separate part of the program called the enforcement policy. FABLE prevents a policy from being circumvented by allowing labeled terms to be manipulated only within the enforcement policy; application code must treat labeled values abstractly. Together, these features facilitate straightforward proofs that programs implementing a particular policy achieve their high-level security goals. FABLE is flexible enough to implement a wide variety of security policies, including access control, information flow, provenance, and security automata. We have implemented FABLE as part of the LINKS web programming language; we call the resulting language SELlNKS. We report on our experience using SELlNKS to build two substantial applications, a wiki and an on-line store, equipped with a combination of access control and provenance policies. To our knowledge, no existing framework enables the enforcement of such a wide variety of security policies with an equally high level of assurance. %B IEEE Symposium on Security and Privacy, 2008. SP 2008 %I IEEE %P 369 - 383 %8 2008/05/18/22 %@ 978-0-7695-3168-7 %G eng %R 10.1109/SP.2008.29 %0 Conference Paper %B IEEE International Conference on Services Computing, 2007. SCC 2007 %D 2007 %T Configuration Reasoning and Ontology For Web %A Dana Dachman-Soled %A Sreedhar, V.C. %K Apache server %K Application software %K configuration management %K configuration reasoning %K configuration space %K File servers %K Information security %K Internet %K knowledge representation languages %K logical framework %K logical reasoning %K ontologies %K ontologies (artificial intelligence) %K Orbital robotics %K OWL %K path planning %K Robot kinematics %K Runtime environment %K Taxonomy %K Web infrastructures management %K Web ontology language %K Web server %X Configuration plays a central role in the deployment and management of Web infrastructures and applications. A configuration often consists of assigning "values" to a pre-defined set of parameters defined in one or more files. Although the task of assigning values to (configuration) parameters looks simple, configuring infrastructures and applications is a very complex process. In this paper we present a framework for defining and analyzing configuration of an Apache server. We define the notion of "configuration space" of an Apache server as a set of possible values that can be assigned to configuration parameters. We then define the notion of an "obstacle" and "forbidden region" in the configuration space that should be avoided. We model configuration space using a logical framework based on OWL (Web ontology language). The obstacles and forbidden regions in the configuration space are modeled as constraints in the logical framework. These obstacles and forbidden regions are essentially "anti-patterns" that a typical installation should avoid. Given an instance of a configuration (that is, a "point" in the configuration space) we then check if the instance is "obstacle free" using logical reasoning. %B IEEE International Conference on Services Computing, 2007. SCC 2007 %P 387 - 394 %8 2007/07// %G eng %0 Conference Paper %B IEEE Military Communications Conference, 2007. MILCOM 2007 %D 2007 %T Verified Enforcement of Security Policies for Cross-Domain Information Flows %A Swamy,Nikhil %A Hicks, Michael W. %A Tsang,Simon %K Collaboration %K Computer languages %K Data security %K Educational institutions %K Government %K Information analysis %K Information filtering %K Information filters %K Information security %K Vehicles %X We describe work in progress that uses program analysis to show that security-critical programs, such as cross-domain guards, correctly enforce cross-domain security policies. We are enhancing existing techniques from the field of Security-oriented Programming Languages to construct a new language for the construction of secure networked applications, SELINKS. In order to specify and enforce expressive and fine-grained policies, we advocate dynamically associating security labels with sensitive entities. Programs written in SELINKS are statically guaranteed to correctly manipulate an entity's security labels and to ensure that the appropriate policy checks mediate all operations that are performed on the entity. We discuss the design of our main case study : a web-based Collaborative Planning Application that will permit a collection of users, with varying security requirements and clearances, to access sensitive data sources and collaboratively create documents based on these sources. %B IEEE Military Communications Conference, 2007. MILCOM 2007 %I IEEE %P 1 - 7 %8 2007/10/29/31 %@ 978-1-4244-1513-7 %G eng %R 10.1109/MILCOM.2007.4455189 %0 Conference Paper %B 19th IEEE Computer Security Foundations Workshop, 2006 %D 2006 %T Managing policy updates in security-typed languages %A Swamy,N. %A Hicks, Michael W. %A Tse,S. %A Zdancewic,S. %K Access control %K Computer languages %K Data security %K Database systems %K dynamic queries %K dynamic semantics %K Educational institutions %K high level languages %K Information security %K information-flow policy management %K Lattices %K Network servers %K Operating systems %K policy update management %K Robustness %K role-based security policies %K RT role-based trust-management framework %K Rx security-typed programming language %K security of data %K statically verified transactions %K transitive flows %X This paper presents Rx, a new security-typed programming language with features intended to make the management of information-flow policies more practical. Security labels in Rx, in contrast to prior approaches, are defined in terms of owned roles, as found in the RT role-based trust-management framework. Role-based security policies allow flexible delegation, and our language Rx provides constructs through which programs can robustly update policies and react to policy updates dynamically. Our dynamic semantics use statically verified transactions to eliminate illegal information flows across updates, which we call transitive flows. Because policy updates can be observed through dynamic queries, policy updates can potentially reveal sensitive information. As such, Rx considers policy statements themselves to be potentially confidential information and subject to information-flow metapolicies %B 19th IEEE Computer Security Foundations Workshop, 2006 %I IEEE %P 13 pp.-216 - 13 pp.-216 %8 2006/// %@ 0-7695-2615-2 %G eng %R 10.1109/CSFW.2006.17 %0 Conference Paper %B DARPA Active NEtworks Conference and Exposition, 2002. Proceedings %D 2002 %T A secure PLAN (extended version) %A Hicks, Michael W. %A Keromytis,A. D %A Smith,J. M %K active internetwork %K active networks %K active-network firewall %K Authentication %K authorisation %K Authorization %K Cities and towns %K Computer networks %K Computer science %K cryptography %K functionally restricted packet language %K general-purpose service routines %K Information security %K internetworking %K IP networks %K latency overhead %K namespace-based security %K PLAN %K PLANet %K Planets %K programmability %K Safety %K security architecture %K telecommunication security %K trust management %K two-level architecture %K Web and internet services %X Active networks promise greater flexibility than current networks, but threaten safety and security by virtue of their programmability. We describe the design and implementation of a security architecture for the active network PLANet (Hicks et al., 1999). Security is obtained with a two-level architecture that combines a functionally restricted packet language, PLAN (Hicks et al., 1998), with an environment of general-purpose service routines governed by trust management (Blaze et al., 1996). In particular, we employ a technique which expands or contracts a packet's service environment based on its level of privilege, termed namespace-based security. As an application of our security architecture, we present the design and implementation of an active-network firewall. We find that the addition of the firewall imposes an approximately 34% latency overhead and as little as a 6.7% space overhead to incoming packets %B DARPA Active NEtworks Conference and Exposition, 2002. Proceedings %I IEEE %P 224 - 237 %8 2002/// %@ 0-7695-1564-9 %G eng %R 10.1109/DANCE.2002.1003496