TY - CONF T1 - Fable: A Language for Enforcing User-defined Security Policies T2 - IEEE Symposium on Security and Privacy, 2008. SP 2008 Y1 - 2008 A1 - Swamy,N. A1 - Corcoran,B.J. A1 - Hicks, Michael W. KW - Access control KW - Automata KW - Collaborative work KW - Communication system security KW - Computer languages KW - computer security KW - Data security KW - enforcement policy KW - FABLE KW - Government KW - high-level security goals KW - information flow KW - Information security KW - Language-based security KW - programming languages KW - Programming profession KW - provenance KW - security automata KW - security labels KW - security of data KW - user-defined security policies KW - verified enforcement KW - Web programming language AB - 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. JA - IEEE Symposium on Security and Privacy, 2008. SP 2008 PB - IEEE SN - 978-0-7695-3168-7 M3 - 10.1109/SP.2008.29 ER - TY - CONF T1 - Configuration Reasoning and Ontology For Web T2 - IEEE International Conference on Services Computing, 2007. SCC 2007 Y1 - 2007 A1 - Dana Dachman-Soled A1 - Sreedhar, V.C. KW - Apache server KW - Application software KW - configuration management KW - configuration reasoning KW - configuration space KW - File servers KW - Information security KW - Internet KW - knowledge representation languages KW - logical framework KW - logical reasoning KW - ontologies KW - ontologies (artificial intelligence) KW - Orbital robotics KW - OWL KW - path planning KW - Robot kinematics KW - Runtime environment KW - Taxonomy KW - Web infrastructures management KW - Web ontology language KW - Web server AB - 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. JA - IEEE International Conference on Services Computing, 2007. SCC 2007 ER - TY - CONF T1 - Verified Enforcement of Security Policies for Cross-Domain Information Flows T2 - IEEE Military Communications Conference, 2007. MILCOM 2007 Y1 - 2007 A1 - Swamy,Nikhil A1 - Hicks, Michael W. A1 - Tsang,Simon KW - Collaboration KW - Computer languages KW - Data security KW - Educational institutions KW - Government KW - Information analysis KW - Information filtering KW - Information filters KW - Information security KW - Vehicles AB - 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. JA - IEEE Military Communications Conference, 2007. MILCOM 2007 PB - IEEE SN - 978-1-4244-1513-7 M3 - 10.1109/MILCOM.2007.4455189 ER - TY - CONF T1 - Managing policy updates in security-typed languages T2 - 19th IEEE Computer Security Foundations Workshop, 2006 Y1 - 2006 A1 - Swamy,N. A1 - Hicks, Michael W. A1 - Tse,S. A1 - Zdancewic,S. KW - Access control KW - Computer languages KW - Data security KW - Database systems KW - dynamic queries KW - dynamic semantics KW - Educational institutions KW - high level languages KW - Information security KW - information-flow policy management KW - Lattices KW - Network servers KW - Operating systems KW - policy update management KW - Robustness KW - role-based security policies KW - RT role-based trust-management framework KW - Rx security-typed programming language KW - security of data KW - statically verified transactions KW - transitive flows AB - 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 JA - 19th IEEE Computer Security Foundations Workshop, 2006 PB - IEEE SN - 0-7695-2615-2 M3 - 10.1109/CSFW.2006.17 ER - TY - CONF T1 - A secure PLAN (extended version) T2 - DARPA Active NEtworks Conference and Exposition, 2002. Proceedings Y1 - 2002 A1 - Hicks, Michael W. A1 - Keromytis,A. D A1 - Smith,J. M KW - active internetwork KW - active networks KW - active-network firewall KW - Authentication KW - authorisation KW - Authorization KW - Cities and towns KW - Computer networks KW - Computer science KW - cryptography KW - functionally restricted packet language KW - general-purpose service routines KW - Information security KW - internetworking KW - IP networks KW - latency overhead KW - namespace-based security KW - PLAN KW - PLANet KW - Planets KW - programmability KW - Safety KW - security architecture KW - telecommunication security KW - trust management KW - two-level architecture KW - Web and internet services AB - 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 JA - DARPA Active NEtworks Conference and Exposition, 2002. Proceedings PB - IEEE SN - 0-7695-1564-9 M3 - 10.1109/DANCE.2002.1003496 ER -