@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.}
}
@conference {14723,
	title = {PLANet: an active internetwork},
	booktitle = {IEEE INFOCOM {\textquoteright}99. Eighteenth Annual Joint Conference of the IEEE Computer and Communications Societies. Proceedings},
	volume = {3},
	year = {1999},
	month = {1999/03/21/25},
	pages = {1124-1133 vol.3 - 1124-1133 vol.3},
	publisher = {IEEE},
	organization = {IEEE},
	abstract = {We present PLANet: an active network architecture and implementation. In addition to a standard suite of Internet-like services, PLANet has two key programmability features: (1) all packets contain programs; and (2) router functionality may be extended dynamically. Packet programs are written in our special purpose programming language PLAN, the Packet Language for Active Networks, while dynamic router extensions are written in OCaml, a dialect of ML. Currently, PLANet routers run as byte-code-interpreted Linux user-space applications, and support Ethernet and IP as link layers. PLANet achieves respectable performance on standard networking operations: on 300 MHz Pentium-II{\textquoteright}s attached to 100 Mbps Ethernet, PLANet can route 48 Mbps and switch over 5000 packets per second. We demonstrate the utility of PLANet{\textquoteright}s activeness by showing experimentally how it can nontrivially improve application and aggregate network performance in congested conditions},
	keywords = {100 Mbit/s, 300 MHz, 48 Mbit/s, active internetwork, active network architecture, active network implementation, byte-code-interpreted applications, Computer architecture, Computer languages, Computer networks, congested conditions, dynamic programming, dynamic router extensions, Ethernet, Ethernet networks, INFORMATION SCIENCE, Internet, Internet-like services, internetworking, IP, IP networks, link layers, Linux user-space applications, Local area networks, ML dialect, Network performance, networking operations, OCaml, Packet Language for Active Networks, packet programs, packet switching, Pentium-II, performance, performance evaluation, PLAN, PLANet, Planets, programmability features, programming languages, router functionality, special purpose programming language, Switches, telecommunication network routing, Transport protocols, Web and internet services},
	isbn = {0-7803-5417-6},
	doi = {10.1109/INFCOM.1999.751668},
	author = {Hicks, Michael W. and Moore,J. T and Alexander,D. S and Gunter,C. A and Nettles,S. M}
}
@article {12079,
	title = {The SwitchWare active network architecture},
	journal = {IEEE Network},
	volume = {12},
	year = {1998},
	month = {1998/06//May},
	pages = {29 - 36},
	abstract = {Active networks must balance the flexibility of a programmable network infrastructure against the safety and security requirements inherent in sharing that infrastructure. Furthermore, this balance must be achieved while maintaining the usability of the network. The SwitchWare active network architecture is a novel approach to achieving this balance using three layers: active packets, which contain mobile programs that replace traditional packets; active extensions, which provide services on the network elements and can be dynamically loaded; and a secure active router infrastructure, which forms a high-integrity base on which the security of the other layers depends. In addition to integrity checking and cryptography-based authentication, security in our architecture depends heavily on verification techniques from programming languages, such as strong type checking},
	keywords = {active extensions, active packets, Authentication, Computer languages, Computer networks, cryptography, cryptography-based authentication, high-integrity base, integrity checking, IP networks, LAN interconnection, mobile programs, network operating systems, packet switching, programmable network infrastructure, programming languages, Protocols, Safety, safety requirements, scalability, secure active router infrastructure, Security, security requirements, services, strong type checking, Switches, SwitchWare active network architecture, telecommunication network routing, Tin, usability, verification techniques},
	isbn = {0890-8044},
	doi = {10.1109/65.690959},
	author = {Alexander,D. S and Arbaugh, William A. and Hicks, Michael W. and Kakkar,P. and Keromytis,A. D and Moore,J. T and Gunter,C. A and Nettles,S. M and Smith,J. M}
}
@article {17301,
	title = {Multiparty Grammars and Related Features for Defining Interactive Systems},
	journal = {IEEE Transactions on Systems, Man and Cybernetics},
	volume = {12},
	year = {1982},
	month = {1982/03//},
	pages = {148 - 154},
	abstract = {Multiparty grammars are introduced which contain labeled nonterminals to indicate the party that produces the terminal string. For interactive person-computer systems, both the user commands and system responses can be described by the linked BNF grammars. Multiparty grammars may also be used to describe communication among several people (by way of computers or in normal dialogue), network protocols among several machines, or complex interactions involving several people and machines. Visual features such as underlining, reversal, blinking, and color, window declarations, and dynamic operations dependent on cursor movement are also covered.},
	keywords = {Application software, Computer aided instruction, Computer displays, Computer languages, Computer networks, Debugging, HUMANS, interactive systems, Protocols, Writing},
	isbn = {0018-9472},
	doi = {10.1109/TSMC.1982.4308798},
	author = {Shneiderman, Ben}
}
@article {17195,
	title = {Human Factors Experiments in Designing Interactive Systems},
	journal = {Computer},
	volume = {12},
	year = {1979},
	month = {1979/12//},
	pages = {9 - 19},
	abstract = {Successful industrial design gracefully unites esthetics and function at minimum cost. However, designers face special problems when they apply their skills to interactive computer systems.},
	keywords = {Application software, Computer languages, Design engineering, Home computing, human factors, interactive systems, Process design, Testing},
	isbn = {0018-9162},
	doi = {10.1109/MC.1979.1658571},
	author = {Shneiderman, Ben}
}
