@conference {14696,
	title = {Fable: A Language for Enforcing User-defined Security Policies},
	booktitle = {IEEE Symposium on Security and Privacy, 2008. SP 2008},
	year = {2008},
	month = {2008/05/18/22},
	pages = {369 - 383},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {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.},
	keywords = {Access control, Automata, Collaborative work, Communication system security, Computer languages, computer security, Data security, enforcement policy, FABLE, Government, high-level security goals, information flow, Information security, Language-based security, programming languages, Programming profession, provenance, security automata, security labels, security of data, user-defined security policies, verified enforcement, Web programming language},
	isbn = {978-0-7695-3168-7},
	doi = {10.1109/SP.2008.29},
	author = {Swamy,N. and Corcoran,B.J. and Hicks, Michael W.}
}
@conference {14755,
	title = {Verified Enforcement of Security Policies for Cross-Domain Information Flows},
	booktitle = {IEEE Military Communications Conference, 2007. MILCOM 2007},
	year = {2007},
	month = {2007/10/29/31},
	pages = {1 - 7},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {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{\textquoteright}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.},
	keywords = {Collaboration, Computer languages, Data security, Educational institutions, Government, Information analysis, Information filtering, Information filters, Information security, Vehicles},
	isbn = {978-1-4244-1513-7},
	doi = {10.1109/MILCOM.2007.4455189},
	author = {Swamy,Nikhil and Hicks, Michael W. and Tsang,Simon}
}
@conference {14706,
	title = {Managing policy updates in security-typed languages},
	booktitle = {19th IEEE Computer Security Foundations Workshop, 2006},
	year = {2006},
	month = {2006///},
	pages = {13 pp.-216 - 13 pp.-216},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {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},
	keywords = {Access control, Computer languages, Data security, Database systems, dynamic queries, dynamic semantics, Educational institutions, high level languages, Information security, information-flow policy management, Lattices, Network servers, Operating systems, policy update management, Robustness, role-based security policies, RT role-based trust-management framework, Rx security-typed programming language, security of data, statically verified transactions, transitive flows},
	isbn = {0-7695-2615-2},
	doi = {10.1109/CSFW.2006.17},
	author = {Swamy,N. and Hicks, Michael W. and Tse,S. and Zdancewic,S.}
}
@article {12094,
	title = {Wireless Network Security and Interworking},
	journal = {Proceedings of the IEEE},
	volume = {94},
	year = {2006},
	month = {2006/02//},
	pages = {455 - 466},
	abstract = {A variety of wireless technologies have been standardized and commercialized, but no single technology is considered the best because of different coverage and bandwidth limitations. Thus, interworking between heterogeneous wireless networks is extremely important for ubiquitous and high-performance wireless communications. Security in interworking is a major challenge due to the vastly different security architectures used within each network. The goal of this paper is twofold. First, we provide a comprehensive discussion of security problems and current technologies in 3G and WLAN systems. Second, we provide introductory discussions about the security problems in interworking, the state-of-the-art solutions, and open problems.},
	keywords = {3G mobile communication, 3G systems, Authentication, Bandwidth, Communication system security, computer network security, computer security, Data security, internetworking, Land mobile radio cellular systems, Paper technology, security architectures, security of data, telecommunication security, wireless communication, wireless communications, Wireless LAN, wireless network security, Wireless networks, wireless technologies, WLAN systems},
	isbn = {0018-9219},
	doi = {10.1109/JPROC.2005.862322},
	author = {Shin,M. and Ma,J. and Mishra,A. and Arbaugh, William A.}
}
@conference {14725,
	title = {Practical programmable packets},
	booktitle = {IEEE INFOCOM 2001. Twentieth Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings},
	volume = {1},
	year = {2001},
	month = {2001///},
	pages = {41-50 vol.1 - 41-50 vol.1},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {We present SNAP (safe and nimble active packets), a new scheme for programmable (or active) packets centered around a new low-level packet language. Unlike previous active packet approaches, SNAP is practical: namely, adding significant flexibility over IP without compromising safety and security or efficiency. In this paper we show how to compile from the well-known active picket language PLAN to SNAP, showing that SNAP retains PLAN{\textquoteright}s flexibility; give proof sketches of its novel approach to resource control; and present experimental data showing SNAP attains performance very close to that of a software IP router},
	keywords = {active picket language, Application software, complier, Contracts, Data security, efficiency, Explosives, INFORMATION SCIENCE, Internet, IP, IP networks, low-level packet language, packet switching, performance, PLAN, practical programmable packets, program compilers, Protection, resource control, Resource management, safe and nimble active packets, Safety, Security, SNAP, software IP router, Software performance, telecommunication security, Transport protocols},
	isbn = {0-7803-7016-3},
	doi = {10.1109/INFCOM.2001.916685},
	author = {Moore,J. T and Hicks, Michael W. and Nettles,S.}
}
@article {12089,
	title = {Secure quality of service handling: SQoSH},
	journal = {IEEE Communications Magazine},
	volume = {38},
	year = {2000},
	month = {2000/04//},
	pages = {106 - 112},
	abstract = {Proposals for programmable network infrastructures, such as active networks and open signaling, provide programmers with access to network resources and data structures. The motivation for providing these interfaces is accelerated introduction of new services, but exposure of the interfaces introduces many new security risks. We describe some of the security issues raised by active networks. We then describe our secure active network environment (SANE) architecture. SANE was designed as a security infrastructure for active networks, and was implemented in the SwitchWare architecture. SANE restricts the actions that loaded modules can perform by restricting the resources that can be named; this is further extended to remote invocation by means of cryptographic credentials. SANE can be extended to support restricted control of quality of service in a programmable network element. The Piglet lightweight device kernel provides a {\textquotedblleft}virtual clock{\textquotedblright} type of scheduling discipline for network traffic, and exports several tuning knobs with which the clock can be adjusted. The ALIEN active loader provides safe access to these knobs to modules that operate on the network element. Thus, the proposed SQoSH architecture is able to provide safe, secure access to network resources, while allowing these resources to be managed by end users needing customized networking services. A desirable consequence of SQoSH{\textquoteright}s integration of access control and resource control is that a large class of denial-of-service attacks, unaddressed solely with access control and cryptographic protocols, can now be prevented},
	keywords = {Acceleration, Access control, active networks, ALIEN active loader, Clocks, Computer network management, cryptographic credentials, cryptography, customized networking services, Data security, Data structures, denial-of-service attacks, interfaces, Kernel, loaded modules, network resources, network traffic, open signaling, packet switching, Piglet lightweight device kernel, programmable network element, programmable network infrastructures, Programming profession, Proposals, quality of service, remote invocation, resource control, restricted control of quality of service, SANE, scheduling, scheduling discipline, secure active network environment architecture, secure quality of service handling, security infrastructure, security risks, SQoSH, SwitchWare architecture, telecommunication security, tuning knobs, virtual clock},
	isbn = {0163-6804},
	doi = {10.1109/35.833566},
	author = {Alexander,D. S and Arbaugh, William A. and Keromytis,A. D and Muir,S. and Smith,J. M}
}
@article {12103,
	title = {Security for virtual private intranets},
	journal = {Computer},
	volume = {31},
	year = {1998},
	month = {1998/09//},
	pages = {48 - 55},
	abstract = {As telecommuting grows, businesses must consider security when extending their network environment to employees{\textquoteright} homes. Researchers at the University of Pennsylvania have addressed the problem with smart cards, operating system modifications, and network authentication. We note the distinction between trust and integrity: trust is determined through the verification of components and the dependencies among them, while integrity demonstrates that components haven{\textquoteright}t been modified. Thus integrity checking in a trustworthy system is about preserving an established trust or trust relationship. Our solution to the challenge of isolating functional roles that may share a single hardware platform is called secure identity based lending (SIBL). SIBL provides multiple personalities by partitioning the hard drive into n+1 partitions, where n is the number of supported personalities. All personalities use the system partition for core operating system components and shared applications. Each of the personalities is also associated with one of the remaining partitions, which are encrypted using a symmetric algorithm},
	keywords = {businesses, Clouds, Companies, core operating system components, cryptography, Data security, employee homes, encryption, functional roles, hard drive, Home computing, home working, integrity checking, Internet, Local area networks, multiple personalities, network authentication, network environment, operating system modifications, Operating systems, Roads, secure identity based lending, security management, security of data, shared applications, SIBL, single hardware platform, smart cards, symmetric algorithm, system partition, telecommuting, Teleworking, trust relationship, trustworthy system, virtual private intranets},
	isbn = {0018-9162},
	doi = {10.1109/2.708450},
	author = {Arbaugh, William A. and Davin,J. R and Farber,D. J and Smith,J. M}
}
