#ABSTRACT#1# Above all, it is vital to realise that completely guaranteed behaviour is impossible and that there are inherent risks in relying on computer systems in critical environments. The unforeseen consequences are often the most disastrous. [Neumann 68] Section 1 of this survey reviews the current state of the art of system reliability, safety and fault tolerance. The emphasis is on the contribution of software to these areas. Section 2 reviews current approaches to software fault tolerance. It discusses why some of the assumptions underlying hardware fault tolerance do not hold for software. It argues that the current software fault tolerance techniques are more accurately thought of as delayed debugging than as fault tolerance. It goes on to show that in providing both backtracking and executable speciifcaitons, logic programing offers most of the tools currently used in softwar fault tolerance. Section 3 presents a generalisation of the recovery block approach to software fault tolerance, called resourceful systems. Systems are resourceful if they are able to determine whetheer they have achieved their goals or, if notk to develop and carry out alternate plans. Section 3 develops an approach to designing resourceful systems based on a functionally rich architecture and an explicit goal orientation. #ABSTRACT#2# Note: Introduction (part of): The generalized Framework for Access Control (GFAC) was introduced as a framework for studying and constructing access control policies in Automated Information Systems (AIS's). This paper discusses a prototyping effort that uses the GFAC concepts. Further, it describes a security policy and the experience gained through implementing a prototype based on that policy. #ABSTRACT#3# Note: This paper provides a very useful view of current (1988) issues, though it will probably be of limited long term interest. It contains a fair amount of 'summary of TNI' type material which clutters it a bit. #ABSTRACT#4# This is the standard reference used for the ALOHA packet radio wide area network from which much of today's technology has sprung. It is essentially a UHF packet broadcast system created by a team at the University of Hawaii. This paper describes the initial implementation of 'pure ALOHA' and the system's configuration,and provides an analysis of predicted channel utilization. The simplest transmission technique is called pure ALOHA. When a node has a packet to transmit it does so immediately; having transmitted the packet, the node waits for an acknowledgement, and if no acknowledgement is received within a time out period, the packet is assumed lost. It is collisions which cause problems, so a collision avoidance mechanism should improve efficiency. In packet radio networks a scheme known as carrier sense multiple access (CSMA) is used. When a node is transmitting all other nodes can receive the transmission, so they can avoid a collision by not transmitting themselves until the channel is free. #ABSTRACT#5# This is the original paper descibing the Z specification language and its meaning; however, both the syntax and the semantics have since been considerably extended and revised. #ABSTRACT#6# Note: This paper outlines the mechanisms used in the secure distributed SunOS. It may be useful as a description of the SunOS model, but seems to leave many questions on general issues unanswered. #ABSTRACT#7# This dissertation concerns the provision of Integrated Services in a local area context, eg on business premises. The term Integrated Services can be understood at several levels. At the lowest, one network may be used to carry traffic of several media - voice, data, images etc. Above that, the telephone exchange may be replaced by a more versatile switching system, incorporating facilities such as stored voice messages. Its facilities may be accessible to the user through the interface of a workstation rather than a telephone. At a higher level still, new services such as multi-media document manipulation may be added to the capabilities of a workstation. #ABSTRACT#8# An automated formal verification study of a commercial network security device, the SmartCrypto, is described. A high level view of relevant formal verification techniques using the m-EVES environment is given. A description of the SmartCrypto is provided, as well as a brief overview of the m-EVES system. The uses and roles of Verification plans, environmental and device-specific models, and other planning techniques are discussed in the context of this case. Observations are made concerning the proof process and the problem of tractability which may apply to similar projects. #ABSTRACT#9# This survey paper describes the alternatives to verification. It primarily concentrates on the tools and techniques that can be used for testing that programs are correct. A brief discussion of proof based systems and of the use of simulations is given. Exhaustive testing of all but the simplest systems is impossible. The paper presents two alternatives to exhaustive testing: functional testing, which ensures that each category of use has been tested, and structural testing, which ensures that each segment of code is tested #ABSTRACT#10# Informal specifications of protocols are often imprecise and incomplete and are usually not sufficient to ensure the correctness of even very simple protocols. Consequently, formal specificaiton methods, such as finite-state models, are increasingly being used. The selection/resolution (S/R) model is a finite-state model with a powerful communcation mechanism that makes it easy to describe complex protocols as a collection of simple finite state machines. A software environment, called SPANNER, has been developed to specify and analyse protocols specified with the S/R model. SPANNER provides the facility to compute the joint behaviour of a number of finite-state machines and to check if the 'product' machine has inaccessible states, states corresponding to deadlocks, and loops corresponding to livelocks. So far, however, SPANNER has had no facility to systematically deal with liveness conditions. For example, one might wish to specify that, although a communication channel is unreliable, a message will get through if it is sent infinitely often, and to check that the infinite behaviour of the protocol viewed as an infinite sequence will always be in some w-regular set (possibly specified in terms of a formula in temporal logic or as an w-automata). In this paper we show that with very minor modifications to the implemented system, it is possible to substantially extend the type of properties that can be specified and checked by SPANNER. This is done by extending the S/R model to include acceptance conditions found in automatons on infinite words, which permits the incorporation of arbitrary liveness conditions into the model. We show how these extensions can be easily incorported into SPANNER (and into essentially any finite-state verification system) and how the resulting system is used to automatically verify the correctness of protocols. #ABSTRACT#11# In this paper we present a generalization of McCullough's restrictiveness model as the basis for proving security properties about distributed system designs. We mechanize this generalization for an event-based model of computer systems in the HOL (Higher Order Logic) system to prove the composability of the model and several other properties about the model. We then develop a set of generalized classes of system components and show for which families of user views they satisfy the model. Using these classes we develop a collection of general system components that are specializations of one of these classes and show that the specializations also satisfy the security property. We then conclude with a sample distributed secure system, based on the Rushby and Randell distributed system design and designed using our collection of components, and show how our mechanized verification system can be used to verify such designs. #ABSTRACT#12# Gypsy was developed as an integrated programming and specification language to support specification, coding and verification of systems software, with particular emphasis on communications software. This paper describes the salient features of Gypsy and gives a worked example of Gypsy's use that encompasses all of its features #ABSTRACT#13# This paper is a good summary of a range of issues and experience in security kernels up to 1980. It outlines the parts of a formal security kernel development methodology, and reviews some of the practical work which has been done in this area. It also presents some of the ways in which the kernel concept is applied to particular problem areas. It finally considers limitations of the kernel methodology. It concludes that the mathematical axioms on which kernel systems are based were very good, but too simple to form a complete practical system. Even practical kernels require too much reliance to be placed in application programs in order to be workable, thus compromising security. #ABSTRACT#14# A paper giving an introductory tutorial on the issues and principles of security kernels. Outlines formal methods but mostly considers the factors involved in designing a practical system. #ABSTRACT#15# Protection models provide a formalism for specifying control over access to information and other resources in a multi-user computer system. Useful protection models must balance expressive power with the complexity of safety analysis, ie. the determination of whether of not a given subject can ever acquire access to a given resource. We argue that, in terms of expressive power, a joint creation operation is a natural candidate for inclusion in an access control model, particularly in the context of integrity considerations. We extend the Schematic Protection Model (SPM) to allow for groups of subjects to jointly create other subjects and objects. We show that the extended model, which we call ESPM, is equivalent in expressive power to the monotonic access matrix model of Harrison, Ruzzo, and Ullman. Additionally, we conjecture that SPM is in fact less expressive than the monotonic access matrix. Thus the joint creation operation appears to have fundamental expressive power lacking in the SPM model. We discuss the safety properties of ESPM. Despite the increase in expressive power, ESPM retains tractable safety analysis for many cases of practical interest. #ABSTRACT#16# Access control models provide a formalism and framework for specifying control over access to information and other resources in multi-user computer systems. Useful access control models must balance expressive power with the decidability and complexity of safety analysis, ie. the determination of whether or not a given subject can ever acquire access to a given object. The access matrix model of Harrison, Ruzzo, and Ullman (HRU) has very broad expressive power. Unfortunately, HRU also has extremely weak safety properties; safety analysis is undecidable for most policies of practical interest. In this paper we show the remarkable result that an alternate formulation of HRU gives us strong safety properties. This alternate formulation is called the Extended Schematic Protection Model (ESPM). ESPM is derived from the Schematic Protection Model (SPM) by extending the creation operation to allow multiple parents for a child, as opposed to the conventional create operation of SPM which has a single parent for a child. It has earlier been shown that ESPM is equivalent in expressive power to HRU. Here we analyze the safety properties of ESPM. We show that, despite its equivalence to HRU, ESPM retains tractable safety analysis for a large class of protection schemes that are of practical interest. #ABSTRACT#17# We offer a concurrency control algorithm for replicated, secure, multi- level databases. In secure databases, single copy techniques cannot avoid indirect channels without subjecting high level transactions to starvation due to malicious low level processes. However, multi- version and replicated databases can avoid starvation problems without introducing indirect channels by maintaining stable copies of old low level data values for use by high level transactions. The algorithm presented here improves on two comparable techniques, a direct multi- version approach of Keefe and Tsai [10] and full replication scheme of Jajodia and Kogan [9]. In the latter, each security level has a container that holds a copy of all lower level data. This paper shows that only a constant number of old copies - two, as it turns out - need be maintained. We argue correctness of our algorithm and demonstrate that the algorithm is free of indirect channels and starvation. #ABSTRACT#18# Protection models provide a formalism for specifying control over access to information and other resources in a multi-user computer system. One such model, the Extended Schematic Protection Model (ESPM), has expressive power equivalent to the monotonic access matrix model of Harrison, Ruzzo, and Ullman. Yet ESPM retains tractable safety analysis for many cases of practical interest. Thus ESPM is a very general model, and it is of interest whether ESPM can be implemented in a reasonable manner. In this paper, we outline a distributed implementation for ESPM. Our implementation is capability-based, with an architecture where servers act as mediators to all subject and object access. Capabilities are made non- transferable by burying the identity of subjects in them, and unforgeable by using a public key encryption algorithm. Timestamps and public keys are used as mechanisms for revocation. #ABSTRACT#19# Separation of duties is an important, real-world requirement that access control models should support. In [13], Sandh introduced the transaction control expression (TCE) for specifying dynamic separation of duties. In this paper we consider the implementation of TCEs in the typed access matrix model (TAM) recently proposed by Sandhu [16]. We show that TAM requires extensions for satisfactory handling of dynamic separation of duties. In particular, dynamic separation requires the capability to explicitly test for the absence of rights in cells of the access matrix. We illustrate how TAM, extended to incorporate such tests, can implement TCEs. We also discuss the impact of checks for absence of rights on safety analysis (i.e., the determination of whether or not a given subject can aquire a given right to a given object). #ABSTRACT#20# An approach to the measurement of software trust is shown to be based on a collection of security and software engineering trust principles. A set of criteria classes consisting of various trust principle combinations is shown to provide a scale for measuring and comparing trust. The system V/MLS secure operating system development approach is used to demonstrate the effect of trust principles in a practical setting. #ABSTRACT#21# Because of the size and complication of ADA, doubts have been raised as to its suitablility for writing secure systems. A system can be considered as 4 levels - applications, applications Runtime Support Library (RSL), security kernel and kernel RSL. As the security kernel is responsible for maintaining separate domains, there is no need (in general) for the Application or its RSL to be trusted. The kernel and its RSL both have to be trusted, but if we restrict the kernel to use the 'PASCAL subset' of ADA, the features provided by the kernel RSL are minimal to non-existent and automatic TLS-to-code correlation becomes feasable. ADA also provides the sort of hardware-oriented features needed for efficiency of the security kernels, and the huge effort invested in the validation suite offers some assurance of compiler correctness. #ABSTRACT#22# The detailed results of a study of the USAF secure computing requirements and the way to achieve them. It goes into considerable detail and includes plans for the development of a prototype secure computer system. This is the document which introduced the reference monitor concept. Although it is quite long it is well worth reading since the problems have not changed significantly and the suggested solutions are the basis for the techniques being used today. There is also an important lesson in how the panel underestimated the difficulty of producing a secure system. #ABSTRACT#23# This paper looks at the problems of network security from a 'new' viewpoint: it shows that the normal concepts used for computer security on single computer systems are applicable to secure network systems. One new concept is introduced, that of a Network Reference Monitor (NRM), and by investigating various configurations of trusted and untrusted computers on a network shows that there are a number of ways of implementing NRMs. It considers the implications of the DoDCSC Criteria if a computer system is to be trusted to handle multilevel data. It is shown that untrusted computers can be attached to a multilevel network via a trusted Network Front End (NFE) which adds appropriate labels to all output and rejects input with unsuitable labels. An unresolved problem is that of connecting to different networks where the granularity of access control and authorisation is not the same; special protocols and/or guard devices may be needed, but such solutions may conflict with other general networking objectives. #ABSTRACT#24# All about proving the information flow properties of parallel programs. This one is for the designers (rather than users) of verification systems. #ABSTRACT#25# An overview of the three part report which can be read separately from them. Well worth reading. #ABSTRACT#26# Tempest is the military term for electromagnetic eavesdropping on emissions from computer equipment. The cost of Tempest eavesdropping equipment can vary from œ3000 to œ150,000, and the costs of protection against these devices varies according to the sophistication of the eavesdropper. Typical security measures include screens attached to individual machines or screened rooms in which all sensitive equipment is placed. Many companies have spent considerable sums on traditional data security methods but electronic eavesdropping can circumvent thes and holders of sensitive information should consder protecting against it. #ABSTRACT#27# The Security Products (SecurityPro) Transition Analysis Facility (STAF) helps both the user and vendor to mitigate interoperability problems, supporting transitions to multilevel security (MLS) integrated systems. This involves identifying and avoiding the many misconceptions and anomalies created by the academic theories and the resulting conventional wisdom formulated during the early days of security research and development. The STAF focuses on user requirements and bases solutions on operational environments and realistic understanding of the strengths, limitations, applicability, and availability of current and future trusted components. The STAF supports MLS command centre enhancements, under the Air Force Electronic Systems Centre (ESC) Portable, Reusable, Integrated, Software Modules (PRISM) program. In addition, the STAF provides engineering support to Government agencies requiring MLS integration. /STAF/Interoperability/MLS. #ABSTRACT#28# This paper examines how Computer Security should be taught in an undergraduate Computer Science curriculum. We will examine: (i) why a Computer Security course should be offered as an elective to undergraduate Computer Science majors; (ii) what should be the prerequisites for that course; and (iii) what should be the content of that course. #ABSTRACT#29# Use of rapid prototyping to develop Multilevel Secure (MLS) systems requires that security be included in the rapid prototyping process. The literature shows some examples of rapid prototyping applied to secure components. However, little guidance is available for using a rapid prototype to develop an MLS system, consisting of multiple components, that can be accredited in the DOD environment. A methodology is proposed for including security in the rapid prototyping process. In this methodology, assurance that security has been correctly incorporated is provided by four foundation documents: the security concept of operations, the security policy, the security architecture, and the certification and accreditation plan. This methodology increases the probability of producing a rapid prototype without serious security shortfalls. #ABSTRACT#30# This paper develops a general mathematical framework in which to study the different flavours of dataflow and considers the operational implications of the different flavors. The main advantage of separating mathematical and operational considerations in this way is that the mathematical underpinnings of operational distinctions are clearly expressed. Another advantage of the framework is that it is the natural middle ground between functional languages and machine architecture. Looked at one way, it yields particular functional languages, and looked at another way, it yields different evaluation strategies for different multiprocessor architectures. #ABSTRACT#31# Although high assurance multilevel secure (MLS) database management systems (DBMSs) are slowly becoming commercially available, these systems are yet to offer a concurrency control protocol that is free of signaling channels and guarantees serializabil- ty (one-copy serializability if multiple versions are kept in the database). Some database vendors have started using in their products concurrency control protocols that are easy to implement and give good performance, even though they do not satisfy the usual serializability requirements. For example, the con- currency control protocol that has been implemented m the commercially available Trusted Oracle MLS DBS generates histories that are level-wise serializable. While level-wise serializability has many desirable properties, it suffers from the inconsistent retrieval problems which may seriously harm database integrity. In this paper, we show that it is possible to meet stricter correctness criteria (such as pair-wise serializ- ability and one-copy serializability) using Trusted Or- acle, provided we have the knowledge of the update transactions that will be executed in the system. We perform a static analysis of the read and write sets of these transactions and, based on this analysis, we con- trol the order of submission of the transactions to the scheduler in such a way that the resultant history en- sures higher correctness level. It is important to note that rather than taking the usual approach of modify- ing the underlying concurrency control protocol such that it meets the stricter correctness requirements, we achieve our goal without modifying the Trusted Oracle concurrency control algorithm in any way. This is because the code that implements the concurrency control is large and complicated and, moreover, the source code for the DBMS is not available since it is provided by the vendors in compiled form to the users. Therefore, it is neither advisable nor possible to ma}e modifications to the concurrency control protocol. #ABSTRACT#32# Over the past few years it has become obvious that the Orange Book is incomplete; integrity and availability are only touched upon. The Orange Book focuses much of its emphasis on disclosure (confidentiality) of data and little to unauthorized modification (integrity) of data. The Canadian Systems Security Centre has begun efforts to create a "Made in Canada" Orange Book. The Canadian Trusted Computer Product Evaluation Criteria, is an attempt to address those areas which were not (or were insufficiently) addressed in the US TCSEC. Two workshops at which Canadian and US industry and government were asked to contribute to a strengthening of the existing US Criteria, have already been held with more planned in the future. The Canadian Criteria is not a definitive answer but an evolutionary step towards incorporation of the requirements of a computer using community. #ABSTRACT#33# A mechanism is presented for ensuring the changes that occur to a system and its data occur in a consistent manner. The mechanism, Process Execution Controls, impose restrictions on the method of access to the data, unlike access controls which impose restrictions upon which users can access the data. This mechanism imposes another layer to the currently existing access control restrictions, but one that is, on the most part, transparent to the user. Although transparent, the system offers the capability to contain viruses to within a given domain. The paper shows two methods of implementation: extending current access control lists, and implementing complementary execution control lists. #ABSTRACT#34# At the 5th Annual Computer Security Applications Conference a paper was presented on a new form of consistency (or integrity) controls. In late 1989 the Government of Canada contracted with Thompson-Foss, Inc. to implement these controls into Trusted Tunis. This paper discusses the Thompson-Foss implementation, how well Process Execution Controls worked, and recommendations for improvement. #ABSTRACT#35# The Cambridge Distributed Computing System (CDCS) was designed some ten years ago and was in everyday use at the Computer Laboratory until December 1988. An overview of the basic design of CDCS is given, an outline of its evolution and a description of the distributed systems research projects that were based on it. Experience has shown that a design based on a processor bank leads to a flexible and extensible distributed system. #ABSTRACT#36# The development of structuring within operating systems is reviewed and related to the simultaneous evolution of concurrent programming languages. First, traditional, multi-user systems are considered and their evolution from monolithic closed systems to general domain structured systems is traced. Hardware support for protected sharing is emphasised for this type of system. The technology directed trend towards single user workstations requires a different emphasis in system design. The requirement for protection in such systems is less strong than in multi-user systems, and, in a single language system, may to some extent be provided by software at compile time rather than hardware at run time. Distributed systems comprising single user workstations and dedicated server machines are considered and the special requirements for efficient implementation of servers are discussed. The concepts of closed but structured and open system designs are helpful. It is argued that the open approach is most suited to the requirements of single user and distributed systems. Experiences of attempting to implement systems over a closed operating system base are presented. Progress towards support for heterogeneity in distributed systems, so that interacting components written in a range of languages may interwork and may run on a variety of hardware, is presented. The benefits of taking an object orientated view for system-level as well as language-level objects and for specification, generation and design of systems are discussed and work in this area is described. An outline of formal approaches aimed at specification, verification and automatic generation of software is given. Finally, design issues are summarised and conclusions drawn. #ABSTRACT#37# Covert channel analysis is a challenging task, particularly when performed during the development of a large system. Some elements of covert channel analysis, such as timing channel identification and reduction, require techniques currently beyond the state of the art. Performing a useful covert channel analysis during development requires a careful balancing of costs and assurance, and a careful selection of currently available techniques. While it is possible for new research to assist in the covert channel analysis of large systems, developers cannot plan on breakthroughs. This paper discusses available techniques, their limitations and tradeoffs, and makes recommendations for performing covert channel analysis. #ABSTRACT#38# Note: The starting point of the paper seems to be the observation that it is often convenient to be able to describe transactions at different levels of granularity, so why not graft nested transaction theory onto Clarke-Wilson? The rest is detail. The concept of nested transactions is definitely a useful one and may well prove fruitful. However, I found neither the content nor the style of presentation of this talk particularly good. Nonetheless it was of of the two joint winners of the prize for best paper.I canðt help thinking that the Badger formulation could probably be greatly streamlined. It has been pointed out by Dale Johnson of Mitre that the model underlying the ISO language ESTELLE resembles the nested transaction model used here. This might provide a means of improving the presentation and may render it more formal. #ABSTRACT#39# This paper describes a Multinet Gateway System which provides an internet datagram service, and the use of the Gypsy Verification Environment to prove it. Quite a lot of internal detail is given but it is not clear how generally useful it is. #ABSTRACT#40# Note: ANSI SQL is a definition of a standard interface language for relational databases. Its security features are mainly based on access control lists (ACLs) for named database objects. Examples of database objects are tables and views. Since they are attached to objects there can be large numbers of ACLs to maintain for an active database. For example, when a new user is added the database security administrator has a lot of work to do in modifying the ACLs. This makes it difficult to maintain both satisfactory security and administrative efficiency. The paper proposes the use of named protection domains (NPDs) to simplify the problem. An NPD is a set of privileges which are permissions that may be held by a subject to use given operations on given objects. A user may only have one NPD active at any given time. However, this is no disadvantage because there is a hierarchical relationship between NPDs, based on the relation that one NPD may contain another. These NPDs may then be used so that users are grouped according to roles. A new user need only be assigned an NPD (or NPDs). NPDs can be used to form a link between the high level specification of security policy and the low level implementation of ACLs. The concepts have been adopted for a future issue of the ANSI SQL standard. This paper describes an extenstion to ANSI SQL that simplifies security management by reducing the complexity of the access controls on database objects, and by providing users with the flexibility to define administrative roles (like Auditor or Security Administrator) that match their requirements for the separation of duties. The benefit of simplified security management is improved security. The main features of this extension have been implemented in the Oracle RDBMS and have been adopted for a future version of the ANSI SQL standard. This paper focuses on major concepts and issues, not syntax and implementation. The key idea is to allow users to group and name privileges to form named protection domains (NPDs). The Clark-Wilson and Bell-La Padula models are used to illustrate the benfits and limitations of NPDs. The main conclusion is that the naming and abstraction mechanisms provided by NPDs can simplify security management in much the same way that procedures can simplify programming. #ABSTRACT#41# The protocol described by this paper started out as a 'dating' scheme: users can register their wishes, but no-one but the intended dates can read the wishes, and then only if they have registered a matching wish; its requirements for anonymity and authentication are similar to those of electronic voting and oblivious transfer. This paper won the 'best paper' award at the 1985 IEEE Symposium on security and privacy. #ABSTRACT#42# Security auditing systems are used to detect and assess unauthorised or abusive system usage. Until recently, security audits have been confined to a single computer system. Current work examines ways of extending auditing to include heterogeneous groups of computers (distributed systems). This paper examines the issues involved in auditing distributed systems, presents the framework for a distributed auditing system (DAS), and proposes a design for the audit reporting elements of the DAS. #ABSTRACT#43# The VAX/VMS environment provides unique built-in security control features for implementation by a system administrator. However, if the necessary controls are not in place, any or all the VAX/VMS security mechanisms can be easily bypassed. The DEC "Guide to VAX/VMS System Security" manual provides security-related information to increase security on VMS systems, but this manual is over 250 pages long and is difficult for the novice system administrator to follow. Therefore, to assist both novices and experienced system administrators in providing at least the minimal security for their VMS systems, SPARTA developed the "VMS System Security Guideline". This paper summarises the contents of the guideline that is currently being used throughout the Department of Energy (DOE). #ABSTRACT#44# The first published description of what was later to become known as a 'packet switching' system was the 11-volume 'On Distributed Computing', written by Paul Baran of the Rand Corporation in August 1964; a summary of which is available in the this reference. This described a study conducted for the US Air Force on providing a survivable communication system for both voice and data transmission. The system proposed had no critical components within it and used a digital microwave system with integral encryption as its transmission medium. Unfortunately the Air Force did not follow this work up and it disappeared into obscurity until packet switching systems were reinvented a few years later. /network example/WAN/packet switching. #ABSTRACT#45# There is currently only limited assurance that software electronically downloaded from a central source is a faithful copy of the original source software. Current Internet standards for privacy enhancement of electronic mail can also be employed to protect electronic distribution of software. The standards offer disclosure protection, source (sender) authentication, and message integrity services. However, electronic mail is a relatively inefficient means for distributing software. Proposed modifications to the mail privacy-enhancement standards will permit files to be afforded integrity and source authentication protection in a manner compatible with current file transfer conventions. #ABSTRACT#46# Note: Trusted Mach (TMach) is a B3-targeted distributed Unix-like system, being developed by TIS under ARPA sponsorship. It is based on a TMach kernel, which supports a number of trusted servers (including a name server), above which lies the Unix kernel. The presentation described the scheme by which RSA and DES algorithms are used together in TMach. The system uses DES for most communications, with cryptovariables stored in a central key distribution centre (cached locally), and RSA for distribution of DES cryptovariables. #ABSTRACT#47# This paper gives a brief definition of a Trusted Computing Base (TCB), and an outline of the RSRE Secure Communications Processor research, in particular the SCP1 and SCP2 processors. #ABSTRACT#48# This paper gives a revised, compact and symmetric version of the Needam-Schroeder key distribution protocol which gives better protection against replay attacks. Unlike the Denning-Sacco protocol, it does not rely on synchronised date-time clocks #ABSTRACT#49# Multilevel Security (MLS) is an integral requirement of many of our defence systems. Building a system to meet these requirements while still meeting stringent operational needs is quite challenging if not overwhelming. This paper highlights the tasks associated with certifying and accrediting a system to meet the security and operational needs of the end-user, then proposes a framework for integrating these tasks into the development process. #ABSTRACT#50# A discussion of what to do when you find out that you are the victim of a computer crime. It deals with such issues as whether to tell the press and how to handle them if you do, how to determine who did it, whether to involve the police, legal system etc. Unfortunately all the legal details pertain to the US rather than the British legal system. #ABSTRACT#51# An examination of general policy support is undertaken using an abstraction of trusted systems termed the "Universal Lattice Machine". This Policy supportability is applied to selected policies from the literature. It is shown that multinational sharing, Clark & Wilson, dynamic separation of duty, the Chinese Wall security policy, and originator control are supportable in this fashion. A constructive theoretical method of switching between isomorphic representations is presented in an annex. #ABSTRACT#52# Note: This came over as a rather clever but at times seemingly rather desperate defence of the Bell/LaPadula model. Nonetheless a number of important (if not necessarily original) points were made. Bell points out that the term model can be used in science and mathematics in several ways: a. An abstraction upon which analysis can be performed. b. As a 'proof' of consistency of a set of axioms. c. As a definition. It was claimed that the Bell/LaPadula model was intended only to fulfil the first of these and hence criticisms of it on the basis of the other two definitions are misguided. He stresses that there is no reality against which to test a model but only intuitions. In order for any analysis performed on the model to be useful the model must be 'faithful', that is to say it must represent (under a suitable interpretation) all relevant features without distortion. 'Modelling' in the context of computer security has the same connotation as in the fields of science and engineering, that of an abstraction used for the consideration of a problem of interest. One recent criticism of the Bell-LaPadula model confused this notion of 'modeling' with a foundational notion of 'model' or 'interpretation' and, in addition, included intrinsic errors of reasoning. #ABSTRACT#53# Note: Bell describes work carried out on behalf of the Defence Communications Agency. The work is based on the premise that the next generation of military packet switches will need to be treated as trusted systems in the sense of the TCSEC. The paper takes Bell's previous work and applies it to packet switched networks (of the DDN type). The paper is based on an interpretation of the simple security property, the *ð-ðproperty and of a discretionary security property. A number of rules relating to the security properties of actions carried out by the network (eg call connection) on behalf of subjects are described. Theorems which show the rules preserve the security properties are also presented. The contents of the paper refer primarily to the network as a whole and the facilities it supports. An individual packet switch is treated to be just another instance of a general purpose trusted system. The work did not address denial of service nor precedence and priority issues. During his presentation Bell spent a considerable amount of time having to correct errors in the formal portions of the paper! To some extent the work presented has been overtaken by the Trusted Network Interpretation of the TCSEC. A general network interpretation of a standard computer security model is applied to the next generation packet switch levels of discourse, using different interpretations. #ABSTRACT#54# How to go about building an A1 trusted computer system. #ABSTRACT#55# This report (35pp, 37 refs) describes a methodology for constructing verifiable systems from real-world problem to useable machine. It shows how category theory can be used to prove the correspondence of links in the validation chain. #ABSTRACT#56# Fairly heavy introduction to mathematical modelling of secure computer systems. Sets out mathematical notation and a security condition. Proves a 'Basic Security Theorem' and a revised version allowing upgrading of subjects and downgrading of objects and proving that the system remains secure. T128; T131. #ABSTRACT#57# This volume takes the model developed in vols 1&2 and the rules from vol 2 as well as the security condition and star-property and refines them to produce a set of rules which is likely to be more useable. The concept of current security level is introduced and the star-property is revised so that it is expressed in a form which is easier to check in a practical application. The revised form of the star-property is stronger than that given in vol2 and there is an explanation of the states that are now excluded. The model is adapted to fit with a hierarchical view of the objects in the system. The control attribute is adapted so that it becomes decentralised and implicit in the hierarchy. The concept of compatibility is introduced and justified and a new rule is given which preserves compatibility as well as security and star-property. There is a set of useful appendices which give the rules, proofs of the new rules and a notational glossary. #ABSTRACT#58# This is the definitive paper describing the Bell-LaPadula model, which has been very influential on the design of subsequent secure system models. In the model subjects attempt to perform certain operations (read, write, execute or read-write) upon objects. Whether this is allowed is defined by a set of rules based on the operation and the security classes of the subject and object. The fundamental rules are known as the Simple Security Property and the Star Property; these are expressed formally and informally in a variety of forms, which has led to confusion. The model is described in formal mathematical terms as a finite state machine, with the state being an access control matrix. State transitions occur as a result of objects being created, subjects acquiring and releasing privileges, and subjects transfering privileges between themselves. The model presents rules for these operations that ensure that all transitions from a secure state result in a secure state. A formal specification of a system based upon Multics is presented together with proofs that the specified functions conform to the security model. T114; T124. #ABSTRACT#59# Classical cryptographic protocols based on user-chosen keys allow an attacker to mount password guessing attacks. We introduce a novel combination of asymmetric (public-key) and symmetric (secret-key) cryptography that allow two parties sharing a common password to exchange confidential and authenticated information over an insecure network. These protocols are secure against active attacks, and have the property that the password is protected against off-line "dictionary" attacks. There are a number of other useful applications as well, including secure public telephones. #ABSTRACT#60# Computer security is emerging as the business risk of the 1990's for many organisations operating in the commercial sector. Unlike military, government, defense and financial organisations, the mid to low risk commercial sector does not have well-developed security procedures. However, owing to the very different security needs of the commercial sector, it is inappropriate to apply the procedures used by high risk organisations. This paper will identify the characteristic system security concerns of the commercial sector, suggest some solutions and in particular investigate a structured and systematic approach to security assessment in the form of a qualitative based security risk analysis. #ABSTRACT#61# Note: The Hierarchical Model presented in this paper is an extension of the Harrison-Ruzzo-Ullman access matrix model. The system is viewed as a deterministic finite state machine, accepting commands which are sequences of enter and delete operations. These operations add/remove ðtokensð from locations in a global state matrix. Tokens may represent access rights, locks or indices into the matrix itself (e.g. object references). The ðschedulerð of the system takes a set of commands as input, and issues the constituent operations of those commands. Commands may proceed concurrently (the operations of those commands are interleaved), subject to the constraints imposed by locks. A command blocks if it attempts to enter a lock where one exists, or delete a lock where one does not exist. This model does not include any security constraints itself; it claims to be a framework in which to express security predicates, including those which require explicit modelling of synchronisation. The paper includes a discussion of critical regions of commands, serialisability and the nesting of critical regions. There is an example of Bell ð La Padula properties expressed in this model, but this seems fairly contrived, and doesnðt increase confidence that the Hierarchical Model is applicable generally. It is admitted that major covert channel problems exist with this approach, and that non-interference properties cannot be expressed in this model. The paper is confusingly written, and the presentation provided little clarification, being based on an over-complex example. The content of the paper seems to bear little relation to any of the keywords in its title, and it is unlikely that the approach will be of much use. #ABSTRACT#62# This paper presents a synchronization mechanism that communicates information from a writer to a reader without permitting information flow in the reverse direction. The synchronization mechanism takes advantage of a priori knowledge of the semantics of communicated information and is optimal because it does not require blocking, busy wait states, an unbounded number of re-reads of data or inefficient use of system resources. The synchronization mechanism has been implemented in the Trusted Mach Operating System's file system. This paper describes Trusted Mach's file system and shows how performance is enhanced through the use of the synchronization mechanism. #ABSTRACT#63# This paper describes a software development process for developing trusted systems under DOD_STD_2167A. The process is based on an approach which integrates Trusted Computer System Evaluation Criteria requirements into the software development process required by DOD-STD-2167A. The process described in this paper focuses on development of DOD-STD-2167A Data Item Deliverables which have been tailored to include TCSEC deliverables. The paper describes how these items can be produced in a manner which minimizes the impact on cost and budget, while increasing assurance in the product's trustworthiness. #ABSTRACT#64# This is the formal statement (and therefore somewhat mathematical) of the Military Message System model, an example of an application based model. T133; T7. #ABSTRACT#65# SCOMP was the first system to be certified in catagory A1. This required formal specification and verification of not just the security kernel, but also of the trusted software that is allowed to bypass the security kernel. This paper describes the methods used for the SCOMP trusted software. Trusted software is not kernel software, nor access control. It is security relevant, and provides specific functionality and user services. It is trusted to control use of privileges (invoke function; modify attributes), to isolate high integrity users (added integrity; restricts user to class; ensure HI software), and to be functionally correct. Examples of trusted software include secure servers, file access managers (privilege), audit tools (integrity) and database editors and file labellers (correctness). The automated tools for kernel verification are not suitable as the trusted software is designed to violate or extend the normal rules for multilevel security. There can be no global policy; the approach taken was to use Gypsy, and a procedure was developed to ensure a thorough review of the verification evidence for each of the trusted software functions. The major problems were the lack of covert channel analysis tools for Gypsy, and the abstract nature of the Gypsy top level specification which made spec-to-code ('C') correlation difficult and subjective. An appendix lists all the trusted component within the SCOMP system. #ABSTRACT#66# Note: This paper describes a toolset used with HDM in the verification of the US Army Regency Net and the US Army/Air Force AN/GSC-40 series Command Post Terminals. It includes translation tools from Ada to (the HDM specification language) SPECIAL (ATOS) and from data-flow diagrams to SPECIAL ('Bubble to SPECIAL'; BTOS), a 'trustedness analysis tool' (TAT) which identifies components needing to be trusted either for secrecy or integrity, a labeller (which produces labelled SPECIAL, given unlabelled SPECIAL and local and global data dictionaries), a propagator (which fixes any remaining floating labels and flags unresolvable conflicts), and a splitter (which splits large modules of a Formal Top Level Specification into more manageable pieces), and a tool to convert the code into provable formulas. #ABSTRACT#67# Note: Revised version of IEEE Symposium paper. The primary goal of MITRE's compartmented mode workstation (CMW) project was to articulate the security requirements workstations must meet to process highly classified intelligence data. As a basis for the validity of the requirementsdeveloped, a prototype was implemented which demonstrated that workstations could meet the requirements in an operationally useful manner while still remainng binary compatible with the off-the-shelf software. The security requirements developed addressed traditional security concerns (e.g. as found in Department of Defence Trusted Computer Systems Evaluation Criteria) whil also introducing new concepts in areas such as labeling and the use of a trusted window management system. The CMW labeling paradigm is based on associating two types of security labels with objects: sensitivity levels and information labels. Sensitivity levels describe the levels at which objects must be protected. Information labels are used to prevent data overclassification and also provide a mechanism for associating with data those marking that are required for accurate data labeling, but which play no role in access control decisions. The use of a trusted window manager allows users to easily operate at multiple sensitivity levels and provides a convenient mechanism for communicating security informaiton users in a relatively unobtrusive manner. #ABSTRACT#68# Note: Published as Vol 23 No 5 of OSR. #ABSTRACT#69# Note: Report of one of the WIPCIS working groups. #ABSTRACT#70# With the recent advances in the theory of multilevel security in databases the field of knowledge bases has opened. In general this paper raises issues rather than solves them. This paper uses a form of unwinding of the non-interference concept to describe the classification of rules. Rules have dependencies and inferences analogous to databases except that their dependencies are more complex. #ABSTRACT#71# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#72# This is a bibliography of under 2000 books and articles. It makes great claims for comprehensiveness, but contains no mention of acknowledged seminal works in the field, such as those by Donald Bell or Dorothy Denning. Do not waste your money on it. #ABSTRACT#73# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#74# This report describes how a subset of SERCUS has been implemented using Tenl5. SERCUS is a research implementation of a multi-level secure workstation based on the SMITE approach and running a classified document handling application. SMITE is an approach to the construction of secure systems which uses strong typing. Ten15 is an algebraically defined, strongly typed abstract machine running on a VAX station. This work was performed while the author was a Vacation Student at RSRE and used the Ten15 Cross Compilation System as it existed in Summer 1990. #ABSTRACT#75# This is a monograph on the algebraic theory of lattices, aimed at experts in pure mathematics. More than somewhat heavy. #ABSTRACT#76# A readable guide to a variety of algebraic topics; the section on partially ordered sets, lattices and representation is particularly good. #ABSTRACT#77# Note: This paper discusses peer entity identification in the SP3 network layer protocol, and suggests a method for peer entity identification. The solution suggested solves the problem of mapping SP3 users on SP3 provides in a networking environment containing intermediate networks and systems. The paper starts by describing some of the problems involved in peer entity identification. It goes on to describe how these problems are compounded by the connectionless nature of network layer protocols, and the characteristics cryptographic protection. The paper then suggests a solution which offers a dynamic method of performing the mappings from SP3 User to provider. The solution involves new network layer protocol procedures which work with existing routing procedures. The solution identifies a least cost path between the two entities using probe packets. This provides advantages such as the dynamic nature of the solutions, however it also has disadvantages, for example the probe packets can be used as a covert channel. SP3 is a network layer protocol that has been designed to provide security services for network service users. SP3 services can be provided by the system in which the network user resides or by Intermediate systems on the path between the network service users. This paper assumes that the network service users reside in different private internetworks and must traverse a public internetwork to communicate. It is further assumed that SP3 services are being provided by Intermediate systems that reside at the internetwork boundaries. The problem is, in this environment, the mapping from SP3 users to SP3 providers is not simple: multiple SP3 systems can serve the same user. This mapping problem is further compounded by characteristics of cryptographic protection and connectionless network layer protocols. This paper discusses the characteristics of the mapping of SP3 service users to the set of SP3 service providers. This paper also offers a dynamic method of performing this mapping by proposing a new network layer protocol and procedures to work in conjunction with inter-routing domain routing procedures. #ABSTRACT#78# This paper describes a new protocol for remote procedure call aiming to overcome the practical efficiency problems often encountered. The protocol is designed to use datagrams, and relies on each client and service having a private encryption key known only to the client (or service) and the access controller. A client can requests a conversation with a service by asking (a local agent of) the access controller using this private key. The protocol proposed is shown to be secure, and has the property that only one datagram and reply is required to set up the conversation and only one extra datagram and reply (in the RFA and its response) is required to fully establish a service connection. Once running there is no further message overhead. #ABSTRACT#79# The work reported here is the result of an investigation into a global naming service for people, machines, organisations and resources. The authentication scheme is expected to have a long lifetime, and to cope with 10,000 million names, using no centralised resource and no universally distributed information. The usual technique is to have a key distribution centre (KDC) which shares a key or password with each principal, and offers evidence of authenticity about other principals. The scheme presented in the paper extends this standard technique by having a collection of KDCs, pairs of which may possess a pairwise shared key. A relative naming structure can be used so that any principal can (eventually, if a path exists) be authenticated to any other. In practice, what is authenticated is a path of KDCs, and what is being trusted is in each node in that path. Access control lists contain paths or path patterns, and the system can be extended to include symbolic links (aliases). #ABSTRACT#80# Grapevine is a multi-computer system on the Xerox Research Internet. It provides facilities for the delivery of digital messages such as computer mail; for naming people, machines and services; for authenticating people and machines; and for locating services on the internet. This paper both to describes the system of distributed and replicated 'registration' and 'message' servers itself, and serves as a case study of a real application of distributed computing. An important distinction is drawn between 'distributed services', involving multiple computers throughout an internet, and 'replicated services' which can be provided equally well by any of several distinct computers. The paper describes the set of services provided by Grapevine, how its data and function are divided among computers on the internet, and the mechanisms used for functions such as resource location and authentication. It considers in detail selected aspects of Grapevine that illustrate novel facilities or implementation techniques, or that provide insight into the structure of the distributed system. In particular it details the algorithms used to manage update of the distributed registration data bases, for finding a mailbox site and for altering the system's configuration. Finally a summary is given of the current state of the system and the lessons learned from it. #ABSTRACT#81# How to do remote procedure calls. Read this if you intend to design network protocols. #ABSTRACT#82# We present a formal model of security monitoring that distinguishes two different methods of recording information (logging) and two different methods of analyzing information (auditing). From this model we draw implications for the design and use of security monitoring mechanisms. We then apply the model to security mechanisms for statistical databases, monitoring mechanisms for computer systems, and backups, to demonstrate the model's usefulness. #ABSTRACT#83# The Network Time Protocol is being used throughout the Internet to provide an accurate time service. This paper examines the security requirements of such a service, analyzes version 2 of the NTP protocol to determine how well it meets these requirements, and suggests improvements where appropriate. #ABSTRACT#84# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#85# Suppose we have a database of n records each with k fields; we can use multivariate galois polynomials so that when doing statistics we can work on encrypted data and then decrypt the result in order to find mean, variance, etc. The problem is to stop someone who knows how to get certain values from using the method to get ways of getting data that should be inaccessible. In other words, the galois polynomials have to be hidden, but in such a way that getting the information is cheap. In the question period D. Denning pointed out that a paper by Rivest et al. showed how to compromise a system that performed statistics on encrypted data where selection by comparison was possible ('av ages of those with salary>3K'). Such selection is not possible with this system. #ABSTRACT#86# Data management applications that use multilevel DBMS capabilities have the requirement to read and write objects at multiple levels within the bounds of a multilevel transaction. Unfortunately, execution of multilevel transactions cannot generally meet both secrecy requirements and the transaction atomicity requirement used in conventional DBMSs. Aborting or delaying operations occurring at lower security levels based on the results of write attempts at higher security levels creates information flows that violate multilevel security restrictions. In this paper, we offer a model of multilevel atomicity that defines varying degrees of atomicity and recognizes that lower security level operations within a transaction must be able to commit or abort independently of higher security level operations. We provide execution graphs as a tool for analyzing atomicity requirements in conjunction with internal semantic interdependencies among the operations of a transaction. and prove rules for determining the greatest degree of atomicity that can be attained for a given multilevel transaction. Finally, we present several alternative transaction management algorithms that can be used to preserve multilevel atomicity. #ABSTRACT#87# VMS has had functions incorporated in it for some time to enable it to support of mandatory as well as discretionary security. The paper describes, in a fairly turgid and detailed style, the way in which the existing latent support is made use of in Security Enhanced VMS. It is an interesting example, but rather VMS specific #ABSTRACT#88# Risk analysis is required by a number of organisations to provide a basis for deciding which safeguards to implement to protect information systems. A variety of risk analysis techniques and tools have been developed. Each technique or tool is based, implictly or explicitly, on a conceptual model of risk. In this paper, the high-level conceptual model of disclosure risk for information systems used in the Analysis of Networked Systems Security Risks (ANSSR) prototype is presented. #ABSTRACT#89# In this paper, we describe MITRE's experience and lessons learned in performing Security Test and Evaluation (ST&E) for SPADOC 4B. ST&E drew on contractual testing but involved extensive government testing of the system. ST&E included testing in a representative stressed environment and in failure situations. ST&E also involved verification of safeguards from security disciplines other than COMPUSEC, including procedural and physical security. SPADOC 4B has been accredited to operate in multilevel mode. #ABSTRACT#90# In this paper, we discuss lessons learned from the acquisition of a large, complex system to support space-related applications, which requires accreditation in multilevel mode to perform its mission. We address the interplay between security concerns and the mission orientation of the system. We also discuss security concerns related to an evolutionary approach, which is the approach the Government is using to acquire this system. #ABSTRACT#91# Note: Referenced by Gasser M: Building a Secure Computer System. #ABSTRACT#92# The LOCK project intends to demonstrate the proof of principle of innovative approaches to technology, policy and doctrine by integrating these elements into a prototype system. There will be technical demonstrations of this prototype 24 and 42 months into the project. This paper describes the larger demonstration context in which these technical demonstrations reside and provides an initial description of the demonstration to take place at 24 months. #ABSTRACT#93# If you want real proofs of security - machine checked (not machine generated), freely refereeable, comprehensible, integrated crypto- functionality and proof, preventing corruption as well as compromise, supporting sophisticated policies - then the machines must be secured at register level. The Secure ADA Target machine is designed to move the security-related mechanisms into the actual hardware rather than relying on a large amount of trusted software. To a subject the system appears to be capability-based, with a personal Name Space Table (NST) that defines both the objects that can currently be accessed and the permitted access. A special coprocessor called the Tagged Object Processor (TOP) handles a Global Object Table and the subjects' NSTs; when asked to update the NST, it calculates the access rights based on the information in the GOT and the current security state. All access by the CPU to the system bus is via a memory map unit and the current NST, so the MMU, TOP and GOT form a hardware security kernel. The paper describes the TOP in detail, together with the user- visible TOP operations and the TOP-processor interface. The whole design is flexible, so though the initial configuration will be a secure ADA computer, it should be possible to reconfigure and revalidate it for other purposes #ABSTRACT#94# In tomorrow's "brilliant" weapons, next-generation avionic computers will need to orchestrate the actions of many sub-systems while further maintaining the security of sensitive data, the integrity of key data and of system behaviour, and often other key properties. Maintainance of these properties will help ensure that system execution is trustable, conforming to both prescribed policies and expected behaviour. For traditional security (confidentiality) as required by DoD, the policy to be maintained is well understood and essentially application independant. Although the weapon environment will surely render inadequate much of current security engineering practice and likely stress the security technology base, the now familiar, fundamental mechanisims of MAC and DAC will still form the foundation of suitable multi-level security (MLS) maintenance. For integrity maintenance, however, realistic policies are quite application dependant. In general, a specific integrity policy needs to comprehend not only certain behavioral aspects of the overall application, but also of potentially many distinct states within the application. Thus, integrity maintenance requires control derived from a state machine specifying "acceptable" application behaviour. #ABSTRACT#95# An architecture especially adept at security support is outlined. The architecture's fundamental information unit is a 2-tuple, or ordered pair, consisting of a datum word and an associated security tag. As an atomic information unit, datum and tag move around through the architecture in unison as processing proceeds. A security subprocessor always operates on a security tag in synchrony with a fairly ordinary data subprocessor's operation on the associated datum word. The coupled subprocessors provide the overall architecture with efficient, multi-level-secure access control and flow control. The proposed architecture represents advancement of security technology along a unique combination of three fronts; 1) direct hardware support, 2) fine- grained-to-the-word mediation and 3) optimal (minimal) result classification. #ABSTRACT#96# The first attempt at a formal specification of the SCOMP kernel. The project of which this was a part was dropped but this report was produced since a great deal of work had already been done. This document contains a large body of SPECIAL code, the SPECIAL reference manual, and a description of the most significant problems remaining when the project was dropped. Unfortunately, the report is not very readable, and does not draw conclusions #ABSTRACT#97# An interesting paper that categorises the reasons for auditing, written by a member of a team funded by the Canadian DoND to investigate possible solutions. That project showed that it is expensive to retrofit auditing into an existing operating system (as in KVM-370), and useless to put auditing into the back-end (too little information available). The proposed solution is to record every keystroke by the user, and also a sample of the output; the author admits there are problems with this, due to the volume of data and the trust imposed on the system #ABSTRACT#98# This short paper points out a flaw in one of the proposed uses of the algorithm described by Needham and Schroeder. A more complex algorithm which corrects the flaw is presented. #ABSTRACT#99# Note: SMITE Ref: 1007. P C Bottomley and S R Wiseman of the Information Security Research Station, RSRE Malvern; examine the development of RSRE's computer architecture for high assurance multi-level security. This article was first given, in an extended format, as a paper at the 1988 Milcomp Conference and Exhibition. #ABSTRACT#100# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#101# The specification language Z has been applied by the Distributed Computing Software Project to the formal specification of network resource managers or 'services'. The use of a formal language gives a more precise understanding of the behaviour of a service and is a prerequisite for verification of programs which use or implement the service. Additionally, the use of Z combined with informal text is sufficiently readable for the specification to be used for documentation purposes. An introduction is provided to the style of specification devised for the project. A framework for the specification of a variety of network services has been developed. The framework is presented, and then incorporated into an example illustrating the specification of both the user's view and the implementor's view of a simple service. A discussion of the experience gained from the specification and use of example service is also included. #ABSTRACT#102# This book presents the logic system that underlies the SRI Boyer-Moore mechanical theorem prover. It attempts to show how the logic can be used to prove theorems rather than presenting the proofs of specific results. It illustrates a number of proof techniques, including simplification, generalisation and the use of induction. It is claimed that the illustrative proofs in the book were all produced using the Boyer-Moore theorem prover. #ABSTRACT#103# This paper describes the Boyer-Moore theorem prover and its use. The theorem prover is one of the major components of the SRI HDM system for the production of verified programs. It attempts - using techniques such as problem simplification and induction - to discover proofs of theorems generated by Verification Condition Generators; these VCGs analyse specifications and identify conditions that need to be shown to hold. #ABSTRACT#104# Within the last few years the integrity of many computer systems has been violated in a variety of ways, the most prevalent of which has been via "virus" attacks. These attacks feature software which, either intentionally or accidentally, result in a compromise of system security and subsequently result in hundreds of thousands of dollars of damage in the form of compromised/lost data or computer downtime. Currently, most attacks are detected long after the fact. Unfortunately, by the time the intrusion is detected, significant damage is done. In the case of a virus, it is likely to have spread throughout an entire network of computers. With the advent of systems containing additional security features such as access control lists, least privilege, and mandatory access control, the question arises, do these systems meet the challenge of preventing system security violations and containing virus programs while still retaining the "look and feel" of a traditional UNIX system? This paper focuses on the features added to UNIX System V Release 4.1 Enhanced Security (SVR4.1ES) intended to raise the overall level of system security to the B2/F-B2 level. #ABSTRACT#105# The DoDCSC (now the NCSC) have published a set of evaluation criteria for categorising secure systems (the TCSEC); using these criteria, it is possible to assign an evaluation class to a computer system. This paper gives guidelines for deciding whether a system of a given class can be used in a particular environment; the factors taken into account include the spread classification markings on the system, the clearances of the individuals, and whether the system is restricted to running trusted application software. This paper formed the basis of the NCSC publication known as the 'yellow book'. #ABSTRACT#106# Note: This paper presented a design for an email system designed for privacy, to be implemented using cryptography and trusted computer systems for protection. The paper then discussed the trust residing in each part of the design. A series of protocols have recently been published to implement a protected mail service over networks such as Internet; these protocols include key management based on public key cryptography. TIS has developed a prototype system, Tmail, to implement these protocols. Part of Tmail runs on each userðs local host, providing local crtographic services and local key management. There is also a single remote Certification Authority, responsible for generating and signing certificates and also generating ðrevoked certificate listsð. Tmail is implemented using the TMach operating system to provide separation between its processes and between Tmail and the usersð processes. TMach (ðTrusted Machð) is a prototype, multilevel, UNIX- like system, ðdesigned to meetð B3, and implemented on a Sun by TIS. It is based on a kernelised version of the Mach operating system originally developed by Carnegie-Mellon University. The paper describes and analyses each component of Tmail in turn, to determine what security functionality it has to provide for the system as a whole to provide the requisite confidentiality (mail only to be read by the intended recipient), integrity (the ability to detect modifications) and source authentication. While based on the TMach implementation, the analysis would be equally applicable to similarly- structured implementations on different systems. A port to UNIX is underway. TMail is a privacy-enhanced electronic mail system on a trusted operating system base. The use of a trusted computing base affords protection to cryptographic control processes and nullifies vulnerabilities that would exist if the mail system were installed on an untrusted base. This paper describes the TMail cryptographic processes that protect the mail in transit from disclosure, detect modification and assure source authentication. The trusted operating system is used to protect the mail and the cryptographic modules on the host system. The trust requirements for the system are discussed. Both aspects of the system, cryptography and trust, are needed to assure protection for the mail within the broader system in which it exists. #ABSTRACT#107# The US Trusted Computer System Evaluation Criteria, called the TCSEC [TCS85] which was first published in 1983 and revised in 1985 has become an accepted standard for the evaluation of trusted systems. Not only is it used in the US for evaluations by the National Computer Security Center (NCSC), it has also been adopted by NATO for the evaluation of systems for use in NATO installations. More recently, in May 1990, a group of four nations, France, Germany, the Netherlands and the United Kingdom produced a first draft of its Information Technology Security Evaluation Criteria, called the ITSEC [ITS90]. The ITSEC shows clearly that the thinking of the computer security community has been heavily influenced by the TCSEC, but the ITSEC also addresses some issues in ways that are very different from the TCSEC. A meeting was held under the sponsorship of the European Commission in Brussels on September 25-26, 1990 at which members of the four nations discussed their reactions to comments received since the publication of the ITSEC and presented their opinions of changes that should be made to the ITSEC. As a method of understanding the ITSEC more completely, it was analysed to determine the impact that compliance with an F5/E5 rating would have upon a B3 targeted system that is under development. This analysis led to a discussion with ITSEC authors from both Germany and the United Kingdom that helped to clarify many questions concerning specific wording and concepts of the ITSEC and its relationship with the TCSEC. It should be noted that the views presented here are the authors' and not official statements from the various organisations with which they are affiliated. #ABSTRACT#108# This paper reports a feasibility study into the Accent and MACH-1 kernels, which are used as part of the Spice distributed operating systems developed by Carnegie-Mellon University, to see whether they could be made to conform to the Orange Book criteria. #ABSTRACT#109# Note: This paper deals with access control concepts using two example systems. Unfortunately one, Aspen, was never fully implemented. The descriptions of the other were stated in the presentation to be out of date, and are superseded by a paper to be published in the Aerospace conference 1988. #ABSTRACT#110# Note: This paper discusses the access control performed by the TMach kernel. The presentation followed the paper closely. The TMach prototype is based on a version of the Unix-based Mach operating system (from Carnegie-Mellon University) which currently implements Mach functionality but not the Mach structures which are essential for security. Therefore the prototype only provides a ðproof of conceptð ð a full TMach implementation depends on CMU completing Kernelized Mach (expected early 1990). The Mach kernel is the object manager for the basic abstractions of: task (passive execution environment, unit of resource allocation); thread (active unit of execution); message (collection of typed data items); port (message queue); and paging object (secondary storage). Threads within tasks can communicate by message passing, by issuing Kernel Interface Commands, or via memory shared with an offspring. This paper concentrates on the mediation of message passing. Tasks queue and dequeue messages from specific ports, subject to the tasks possessing the relevant ðsendð or ðreceiveð access rights to the ports. It is claimed that since ports represent the ðobjectsð, in the TCSEC sense, control over the transfer of port access rights implies control over information flow. For MAC, the strategy is to label each port with a single security level, and each task with two levels; maximum-write and minimum-read. This enables a uniform treatment of trusted and untrusted tasks (the two levels of an untrusted task are identical). Messages are tagged with the security levels of the sending task; although they are not explicitly labelled with a single security level, they could be implicitly associated with the security level of the ports via which they are transferred. Port access rights are transferred as part of a message, and the kernel mediates such transfers at message receive time. The security policy is expressed as a set of security invariants, which the kernel must ensure are upheld. Mechanisms exist to close the potential covert channels arising from ports filling up or being deallocated. DAC was claimed to be a harder problem for the TMach designers, since the underlying Mach kernel does not support user identities. By itself, the TMach kernel does not provide full TCSEC DAC, but does provide mechanisms which could support a full DAC implementation. The TMach kernel associates a user-id with each task. Messages are tagged by the sending task with the user-id of the intended recipient, and the kernel ensures that the actual recipient has the matching user-id. The DAC scheme also includes a system of privileges relating to the transfer of access rights. TMach is not a distributed system; however it is claimed that the design does not preclude distribution. There was some confusion in the presentation over where MAC and DAC are performed, other than in the kernel, and so it is not clear whether this paper completely covered access control in TMach. However, within the scope of message- passing, this seems a sensible approach to access control. #ABSTRACT#111# Note: Trusted Mach (TMach) is a B3-targeted distributed Unix-like system, being developed by TIS under ARPA sponsorship. It is based on a TMach kernel, which supports a number of trusted servers (including a name server), above which lies the Unix kernel. One feature of the system is that all subjects communicate via object- like ports which are monitored by the kernel, and subjects may be granted transmit or receive rights to a port. A formal model of the system is being retrospectively produced. #ABSTRACT#112# Note: i/s as a reprint from the original. #ABSTRACT#113# Note: This paper was inspired by the work of Clark and Wilson, and the WIPCIS initiative. It describes a commercial confidential policy as opposed to a national security policy. The Chinese Wall Security Policy is a real commercial policy which can be formally modelled. All corporate information is stored hierarchically in three levels. At the lowest level are individual items of information (cf objects in BLP). All objects concerning the same corporation are grouped together in a company dataset. At the highest level, all company datasets whose corporations are in competition are grouped together in conflict of interest classes. Initially, a user (cf subjects in BLP) has complete freedom of access. Once his initial choice has been made a Chinese Wall is created for him around the chosen dataset, and any other dataset within the same conflict of interest class is deemed to be on the ðwrong side of the wall.ð The user is still free to access any dataset in a different conflict of interest class. Subsequent accesses change the shape of the wall to include the new dataset. Thus, the Chinese Wall policy is a combination of free choice and MAC. Since not all information is price sensitive, and the sensitivity of information can be reduced over time, there exists sanitised data which anyone can access. In the paper, analogies with the Bell-LaPadula (BLP) model are considered. In the formal model (see Annex A), two of the axioms are analogous to the simple security and *-properties. However, the Chinese Wall cannot be correctly represented by BLP. It differs from BLP in that it is time dependent and considers past accesses. This work appears to be a useful paper in commercial computer security. #ABSTRACT#114# In this paper, we present the rationale behind the requirements for cryptographic implementations which have been integrated into version 3.0 of the Canadian Trusted Computer Products Evaluation Criteria. We believe that an integrated set requirements for cryptography is an essential step towards bridging the gulf between communications and computer security. #ABSTRACT#115# Note: What makes this paper significant is that the program verification system described, Cartesiana, is said to be currently in use for the development of a provably secure system in a pilot project in W. Germany. It is also described as a prototype. The level of assurance sought in the pilot project calls for code verification i.e. beyond A1, or Q6/Q7 in the FRG quality scale. The paper is in three parts. The first of these is advocacy for the correctness-by-construction approach to program verification, as opposed to an after-the-fact verification of a given program. Correctness-by-construction is concerned with top-down refinement, with at each step a formal justification accompanying the refinement step. With program development, the steps may be quite small. Textbooks such as Gries, cited by the authors, cover this topic. The second part of the paper, which is most of it, is a very long and detailed treatment of an example of development according to correctness by construction. A proof is sketched that pre- and post- conditions preserve invariants of state (taken as the security-property of interest). An algorithmic refinement is undertaken, starting from pre- and post-conditions, and at each step transforming the Hoare triples to derive proof-obligations from the proof rules of the programming language. The refinement example is presented entirely as a pencil-and-paper exercise, with nothing to relate it specifically to Cartesiana. As far as I can tell, there seems to be nothing fundamentally new here: these are basically the techniques described in, for example, Gries. There is no presentation of a rationale as such, for choice of the refinement steps. While this may be an example of a development method I am unable to tell what the method actually is, other than the need to do after-the- fact justifications at a fine grain. Moreover, the amount of detail in the examples is excessive. The final part of the paper is a rather short and vague description of the Cartesiana tool. The interesting question is whether the tool offers any support specifically for the program-construction process (other than containing in its ðrule-baseð a theory of Hoare triples for the programming language). I cannot find any explicit statement in the paper to this effect. There is machinery for programmed tactics (ðmacrosð) but this is described as under evolution. The Cartesiana tool is generic with regard to programming language, syntax, logic. No indications are given as to any successful or experimental applications of the method or the tool. No references are given to any other description of the tool. Cartesiana is a system to support the construction of software on the basis of formal methods. It is currently being used for the development of a provably secure system in a pilot project in the Fed. Republic of Germany. The quality criteria applied go beyond A1 and include program level verification. The Cartesiana approach to meet these criteria emphasises constructive techniques: proof rules are used to derive a solution in such a way that development and verification are closely combined. Rules and specified formal requirements guide the development process. Some of the methodological aspects are illustrated by way of example. A concise overview over the main functionalities of the system is given. #ABSTRACT#116# Note: Ulysses is a collection of tools designed to assist in the design and verification of secure computer systems. It includes a process definition tool, which looks like a programming language (but with formal back-up), and a text/diagram system design language not dissimilar to MASCOT. There is in addition a proof system including 'tactics' (incomplete proofs), which enable more complex proofs to be built up from the six simple rules originally provided; a 'tactic library' is now under development. The security policy for this project is based on noninterference- style conditions, and it is expected that by use of McCullough's 'restrictiveness' (or 'hook-up') property, the target system may be designed in small pieces and 'hooked up' without loss of verifiability. #ABSTRACT#117# This paper will address the logistics of distributing a smart token on a computer system. A smart token is an identification and authentication device for a host computer system. This paper will address the logistics from four perspectives. The first perspective will discuss why the smart token, WATCHWORD Generator was implemented on DOCKMASTER. A cost analysis, including procurement of the smart token, batteries, man hours, and maintenance is the second perspective. The third perspective discusses how the smart token will enhance the security of the host computer system. How DOCKMASTER will respond when a use is trying to access the system with the WATCHWORD Generator implemented is the fourth perspective. With a successful method of identifying and authenticating users of the computer system, the system is less susceptible to penetration. #ABSTRACT#118# This paper proposes a new methodology for risk assessment in the computer field, where attacks are more often deliberate than in other fields, and suggests research directions. #ABSTRACT#119# This paper describes a software subsystem that can be added to each of a set of physically interconnected UNIX or UNIX look-alike systems, so as to construct a distributed system which is functionally indistinguishable at both the user and the program level from a conventional single-processor UNIX system. The techniques used are proposed to be applicable to a variety of both local and wide area networks, and to enable all issues of inter-processor communication, network protocols, etc., to be hidden. It gives a brief account of experience with such a distributed system, which was operational on a set of PDP11s connected to a Cambridge Ring. The final sections compare this scheme to various precursor schemes and discuss its potential relevance to other operating systems. #ABSTRACT#120# In 1950, on a subject seemingly unrelated to information security, Alan Turing proposed a definition of machine intelligence. Turing's idea is his well known "Turing Test". In this paper, I will show how the Turing Test provides a very simple yet very general characterization of non- information flow in multilevel information systems. Despite its conceptual simplicity, the Turing Test provides the study of information flow with an extremely useful notion which seems to be a significant departure from other current information flow theories. Turing's powerful idea is that information entropy is represented as uncertainty about the mathematical definition of a system, rather than as some function of the direct behavior of the system. #ABSTRACT#121# This paper addresses the dual problems of monitoring a contractors's performance and providing adequate computer security within the Federal government environment. Contractors perform many of the government's computer functions, therefore security must be a part of their services and products. How does the government know that the contractors' are performing the computer security function in an acceptable manner, and that they have the proper level of awareness, commitment, and skills to provide this security? Guidance for determining the contractor's experience, and assuring performance, as they relate to computer security, are contained in this paper. The paper is intended for use by computer security officers, computer resources management and technical staffs, and contracting officers, as well as by educators who are responsible for training the government personnel. Although the paper is directed toward those individuals within the Federal government, most of what is stated would also be of value to individuals who are working for a commercial organisation. The contents of the paper is based on the author's thirty years of experience working as a computer manager, technician, and educator within both the Federal government and commercial environments. #ABSTRACT#122# This short paper describes in general terms what is involved in performing a system security audit (also known as an internal audit or security review). The audit determines the adequacy of physical security, access to programs and data, and controls to ensure continued integrity of the system. Points to look for during a review are outlined. A description is given of the way in which the computer itself can assist the auditor, with programs to check data integrity and review or analyse audit trails created during normal running. This analysis can be performed while the computer is running. #ABSTRACT#123# Note: This paper presents a model of security for an aspect of relational databases. It tackles the issue of referential secrecy: the analogue of the usual referential integrity. It considers the requirements for constraints on relationships between the security characteristics of related data. Attempts to remove covert channels arising from the normal integrity constraints of the relational data model (i.e. entity integrity and referential integrity) and which retain an operational DBMS result in the problems of polyinstantiation, referential ambiguity and uncontrolled dangling references. The view is taken that such an approach, as in the SeaView model, results in unwarranted complication of the semantics of the data model. Automatic polyinstantiation is not permitted in this model. However, there is a rudimentary mechanism for providing cover values. The objects in this model are tuples. Referential secrecy requires that the security class of a tuple which contains a reference must dominate that of the tuple referred to. Operations are possible which would cause violations of referential integrity: „ insertion of a tuple with a foreign key „ deletion of a tuple which is referred to by a foreign key. Additionally action might be useful on deletion of a tuple with a foreign key. In the draft update to SQL choices of resulting action may be defined for each foreign key in each relation. These are SET NULL, SET DEFAULT and CASCADE. The operations above which are relevant to referential integrity can cause violations of referential secrecy. The paper defines analogous actions to be taken as a result of referential secrecy: „ DEFAULT, which rejects an operation if it results in a violation of referential secrecy; „ REJECT HIGH, which rejects insertions with references that strictly dominate the tuple referred to; „ ACCEPT LOW, which permits dangling references for views at some security classes by permitting one tuple to contain a reference to a tuple which it does not dominate; „ UPGRADE, where an attempted insertion is upgraded until it satisfies the referential secrecy requirements. REJECT HIGH is not security critical. All the others result in covert channels which, in any implementation of this model must be monitored. Appropriate actions must be taken as a result, such as slowing down the channel or shutting down the DBMS. The constraints proposed in this paper are readily enforceable by a DBMS, but there are some limitations in the protection which may be provided, in particular those relating to the values of data. This is a very practical solution to a difficult problem and forms a reasonable compromise between the requirements for freedom from covert channels and the semantic problems associated with the removal of these covert channels. This paper presents a referential secrecy model that simplifies automatic data classification within a relational database. The model captures the secrecy semantics that reflect the dependencies among foreign key references. These dependencies form the basis for specifying classification constraints, without the complexity of rule- based or view-based mechanisms. The secrecy semantics are expressed within the database schema as parameters to the foreign key definitions. Data classification is a function of the access class labels of the foreign key reference tuples, as well as the access class of the subject. #ABSTRACT#124# Proposes a security mechanism, the integrity lock, which can be retro- fitted to existing database systems. The mechinism is briefly described, and shown applied to an INGRES database running under UNIX. #ABSTRACT#125# Note: PhD Thesis. #ABSTRACT#126# Note: Published as Vol 23, No 5 of OSR. #ABSTRACT#127# Note: Also in: Gehani N, McGettrick A D (eds): Software Specification Techniques, Addison-Wesley, International Computer Science Series, ISBN 0-201-14320-9. #ABSTRACT#128# This booklet is issued in connection with CA's 'Top Secret' security software package. It gives some helpful hints for considering the problems of installing security software, mainly from the commercial point of view. #ABSTRACT#129# In this paper we augment the syntax of CCS by introducing a priority operator. A new equivalence relation which is based on Milner's strong observational equivalence [11] is defined and proved to be a congruence. We also give some examples which illustrate the use of the operator and emphasise the novelty of the approach used to introduce the notion of priority to process algebras. #ABSTRACT#130# This memo assesses the effectiveness of using algebraic techniques in the compilation of microcode. Microcode for an example system, the SMITE secure processor, is considered. #ABSTRACT#131# The paper describes a machine being developed by Sytek for guard applications, being a small special-purpose device that can be added to an existing system to provide a physically isolated security mechanism. Separate buses ensure that a slave domain (protected environment in which a process executes) cannot communicate directly with other domains; an interdomain communication board (ICB) connects slave busses to a master bus, through which interdomain traffic is possible subject to the control of the master domain. The core software running in privileged mode in the master domain controls the ICB; this software (in ROM), the master domain hardware and the ICBs together form a reference monitor, with the security policy controlled by application software in the master domain. The paper ends with a brief discussion of the verification considerations relevant to such a stand-alone device. #ABSTRACT#132# Note: This paper presents a series of rules for the Operation of a Secure Multilevel system, covering not just disclosure but also integrity, audit, roles and inference. It is rather difficult to read, and contains some oddities - for example, the sensitivity lattice appears to be converted without justification to a total order, and the rules on disclosure phrased accordingly. #ABSTRACT#133# Note: Available as Datapro Report IS50-560-101. #ABSTRACT#134# Note: This paper discusses various issues raised in the design phase for a distributed secure operating system that is intended to run on a variety of hosts and over a variety of network types. The operating system, SDOS, is based on the object-oriented Cronus system, where an object is an instance of an abstract data type, and the operations on it are supported by the object manager for that type. In theory, the security policy of the system is the security policy of the various abstract data types, but the authors see difficulties where the users can add their own type definitions. Consequently, they have split the policy into two parts, one covering message passing and the other concerning information flow within each system component. The inter-component message passing rules are simple: each system component has a clearance, and is constrained to send and receive messages within its clearance. For the information flow within a component with a multiclass clearance, the McCullough hookup-secure information flow policy is used, and a component is called restrictive if it has this property. It is not stated as such, but the message- passing rules would appear to be intended to provide the environment within which the restrictive property is composable. As part of the SDOS project, it was proven that the restrictive property was implied by a combination of the (non-composable) weak- noninterference property and 'various other simple properties'. A technique was developed to prove, using Gypsy, that a design had these properties and so was restrictive. The problem of covert channels is briefly discussed, and they are categorised into two types - those that are inherent in the design of the operating system, and those that arise through the use of an untrusted medium; in the latter case, reference is made to 'someone called Girling' who was misquoted as showing it was impossible to decrease the bandwidth of such channels without similarly degrading the useful bandwidth. Discusses some issues in distributed system security, in the context of the design of a secure distributed operating system. The design is targeted for an A1 rating. Some new developments in formal verification methods are reported. Distributed system security is contrasted with single-host and network security, and described in the context of the TNI. Problems unique to distributed system security are discussed. An argument is made for implementing security features in higher layers, corresponding rougly to the session through application layers of the OSI model. A new security policy, based on message- passing rather than reads and writes, is described. The SDOS design is summarized. #ABSTRACT#135# A document retrieval system is a specific type of distributed processing which has its own particular security requirements. This paper proposes a model for secure delivery of documents and describes a prototype system, based on earlier work on secure electronic mail and automated document delivery systems, being developed at University College London. In the proposed architecture, security protection is provided for document requests and the actual documents delivered. E-mail protocols are used for document requests and delivery, although file transfer protocols could be used in some circumstances. The paper begins with a discussion of the document delivery system background and then sets out the client-server model for the secure system. The security philosophy, requirements, policy, and techniques are dealt with next. The criterion for validation is analyzed; the relationship to OSI is shown; implementation issues are discussed and the direction of future efforts is pointed out. #ABSTRACT#136# Note: IXth Plenary Assembly, Melbourne, Australia, November 1988. #ABSTRACT#137# Note: Recommendation Z.110: Criteria for the Use and Applicability of Formal Description Techniques. #ABSTRACT#138# This reference describes the set of protocols used on ARPANET, sometimes referred to as TCP/IP (for the main two protocols: transmission control protocol and internet protocol) #ABSTRACT#139# A summary of the symposium, and short reports on each of the papers - these reports have been added as notes to the relevant enntries in this bibliography. #ABSTRACT#140# This paper describes the differences in philosophy between the treatment of information in industry and by the military, and the ways these differences affect the requirements and practices of the two sectors. The private sector philosophy is that information is an asset, to be protected against disclosure, modification or destruction to a level commensurate with its value. It can be assumed that any attacker will also be working to economic rules, and will not want to get information at any cost. Assets can usually be given a cash value, which will determine the degree of protection required, and the 'bottom line' philosophy rules - if it doesn't further the goal of making money, don't do it. Also unauthorised reading of information is often not considered as significant as unauthorised modification. In both sectors, the major security risk is insiders working within their authorisation, where the presence or absence of a provably secure computing base is irrelevant. The major common interests are fourfold: the need for authentication of people, the need for audit trails, the need to monitor the behaviour of those in employment, and the need for security to be cost effective. It is concluded that research and developments in these fields would be of significant benefit to both sectors. #ABSTRACT#141# A description of an experimental system based on take-grant for deciding whether a particular individual is allowed at this time to do a certain operation on a database. #ABSTRACT#142# The purpose of the study is to identify and model internal controls of Automated Teller Machine (ATM) systems used by the banking industry. A reliability model of internal controls of ATM systems using series, parallel, and simple structures is presented. Control items and relationships are justified based on the engineering, computer, and auditing literatures. Use and limitations of this model are also discussed. An ATM case with fixed controls and a related questionnaire has been developed. A computerized decision aid programmed in the PC BASIC language for assisting design and evaluation of the ATM internal control system has been developed and evaluated. To evaluate the modeling effectiveness, a small group of graduate students in the EDP Auditing master program uses the decision aid to evaluate the ATM case by filling out the questionnaire. Computed values are compared with the user-assigned values to examine differences between model results and human judgments. #ABSTRACT#143# This describes ways of allowing individuals to be known by pseudonyms in different organisations - so making it difficult to build up dossiers on them - while still allowing signed credentials to be transferred. #ABSTRACT#144# This paper reviews some of the available methodologies for producing code that can be verified to obey certain properties. It concentrates on four systems: HDM from SRI (SPECIAL, MLS), FDM from SDC (Ina Jo, ITP), Gypsy from the University of Texas, and AFFIRM from ISI (XIVUS, DTV). Each of these is described in detail by someone who has actually tried to use it, and at the end is a comparison and some general conclusions (such as the fact that all of them require an expert user). #ABSTRACT#145# Note: This paper proposes a modelling scheme suitable for dealing with heterogeneous distributed systems in which the differing operating systems implement the same policies. This is done using a system of 'subject domains' in which each subject has the same clearance. These subject domains may consist of subjects running on more than one machine. The paper appears well-considered and may be worthy of more detailed investigation. #ABSTRACT#146# Note: This paper describes a student project undertaken at the University of Maryland. In order to be undertaken in a limited timescale, a small but realistic security problem was selected, and then a high-assurance solution was attempted. The chosen problem area was the formal specification of a multiparty session protocol, the production of a security model, and the demonstration that the protocol satisfies the model even in the presence of intruders. A multiparty session is characterised by the fact that a number of processes come together and perform some action on a shared system state before resuming independent existence; intruders can be modelled by extra processes listening in to messages and perhaps supressing some and/or inserting their own. The paper starts by defining multipary sessions and introducing a security policy. A model of this policy is then given, taking just over 1 page in the Proceedings, and explained. The paper then goes on to present the FTLS of the multiparty session protocol and its associated key-distribution protocol, and to demonstrate how the FTLS can be machine-proven to be conformant with the security model. The paper is hard-going, but is likely to be worthwhile reading - even if just as an existence proof -for anyone who is going to have to produce a formally- specified and verified system. In this paper we present the formal specification and verification of the multiparty session protocol discussed in (CG88). The notion of intruder processes is introduced to model intruder actions and counter- measures of the trusted computing bases. We argue that multilevel network security can be achieved and verified formally independent of the specific transport-layer protocols even in the presence of intruders through the use of (1) a multilevel secure session protocol and (2) a key-distribution protocol which helps establish message confidentiality and integrity across an untrusted network. Both the formal security-policy model and the formal top-level specification (FTLS) of the multiparty session protocol are written in Ina Jo [SH89]. The inference rules of the logic of authentication [BAN89] are incorporated in Ina Jo transforms to demonstrate the correctness of the key-distribution protocol. Two detailed examples of formal proofs are included. #ABSTRACT#147# The purpose of this paper is to identify the techniques for protection of the Call Detail Records (CDR) in the Federal Government telecommunications systems, such as the FTS2000 and the agency PABX's. The paper contains a description of the CDR data flow, their use in telecommunication and their protection requirements. Description of threats and countermeasures are provided. Recommendations for handling and protection of the CDR data base are made for the following organizations: FTS2000 contractor billing, FTS2000 contractor network engineering, Service Oversight Center and user agencies. #ABSTRACT#148# Most discussions on computer security focus on disclosure. In particular, the U.S. Department of Defence has developed a set of criteria for computer mechanisms to provide control of classified information. However, for that core of data processing concerned with business operation and the control of assets, the primary security concern is data integrity. This paper presents a policy for data integrity based on commercial data processing practices, and compares the mechanisms needed for this policy with the mechanisms needed to enforce the lattice model of information security. We argue that a lattice model is not sufficient to characterise integrity policies, and that distinct mechanisms are needed to control disclosure and to provide integrity. Proc. 1987 IEEE Symp. on Security and Privacy, pp. 184-193 This paper compares the well-known concerns of military computer security, protection against disclosure of sensitive information, with the concerns of commercial security. The commercial world is concerned with security against fraud and error, and thus with data integrity. The mechanisms used to provide security in the commercial world are quite different from those of military security. The two principal mechanisms are: „ the well-formed transaction (for example, in double-entry book- keeping every entry in one account must be balanced by an entry in another); and, „ separation of duty (that the person who authorises a transaction and the person who executes it must be distinct - collusion is then needed to breach security). A model for integrity is developed, with nine rules, which is shown to be superior to the Biba model (inverse Bell & LaPadula) or the lattice model of Lipner at expressing these particular requirements. The central doctrine is the need to control three things together: which user uses which program on which data. Recommendations are made that for better security for industry, systems must provide: „ better user authentication, „ segregation of duties within the security-officer function, and „ better capabilities to govern execution of programs and transactions. In the long term, this could be the most influential single paper of the conference. #ABSTRACT#149# This gives a brief history of the U.S. National Security Decision Directive 145, and the consequent direction taken by the NCSC. The main meat of the paper is an outline for U.S. companies on how to use the Center's facilities. #ABSTRACT#150# This paper presents Strong Dependency. It is rather mathematical. #ABSTRACT#151# Mathematical. Describes a technique for modelling information flow in programs. #ABSTRACT#152# Report of extensive research into programs that propagate certain of their own behaviour into other programs. Results of use of this technique as a penetration attack. Very interesting reading. #ABSTRACT#153# Note: Abstract in TechGnosis June 1989 (PO689-17). Prevention of infection by computer virus can only be guaranteed by limiting information sharing or functionality. This paper examines complexity-based virus detection mechanisms which detect modifications and prevent secondary infections. The philosophical issues involved in providing protection against viruses are discussed and the structure of dependencies within an information system is considered. A mathematical model of change control within a trusted computer system is described and features of the mechanisms used identified. An alternative to dependency relations is proposed. Implementations for untrusted systems are outlined and the optimality of the mechanisms employed considered. The role of the environment in viral protection, practical limits of the techniques proposed and practical implementations of the systems are discussed. #ABSTRACT#154# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#155# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#156# In a multilevel secure database management system (MLS/DBMS), users cleared at different security levels access and share a database consisting of data at different sensitivity levels. A powerful and dynamic approach to assigning sensitivity levels (also called security levels) to data is one which utilizes security constraints or classification rules. Security constraints provide an effective and versatile classification policy. They can be used to assign security levels to the data depending on the content, context, and time. In this paper, we argue that security constraints are a special form of integrity constraints enforced in a MLS/DBMS. As such, they can be handled during query processing, during database updates, or during database design. We then describe in detail the design and implementation of a secure update processor which handles security constraints in a multilevel secure database management system. #ABSTRACT#157# This is the yellow book; it tells procurers how to determine a suitable rating to specify for a secure system depending on factors such as the spread of sensitivity of data and the spread of clearances of the users. #ABSTRACT#158# Note: The State Delta Verification System (SDVS) project is attempting to provide a capability for the formal verification of Ada programs by stages; the initial aim (now complete) is to provide verification of Core Ada, which consists of basic statements and types, and simple I/O). More complicated features of the Ada language are expected to be added in later stages of the project. The 'state deltas' forming the semantic basis of SDVS are generated by a translator consisting of a translator consisting of a parser and two semantic phases, all implemented in Common Lisp (with lazy evaluation). Strong types are chosen and implemented, and scoping is implemented by prefixes. #ABSTRACT#159# Note: Technical Report No 128 (PhD Thesis). #ABSTRACT#160# Note: Technical Report No 119. #ABSTRACT#161# Note: Referenced by T1209. #ABSTRACT#162# A book that achieved brief notoriety by including details of devices to cheat the telephone system (since removed); on the whole, a naive book aimed at naive users. #ABSTRACT#163# Note: This paper presents, with the aid of a scaled-down example, the specification strategy employed in the Secure Military Message System project. The emphasis is on using attempted proofs of security to guide the writing of module specifications, and providing exemplary documentation to assist the designers and programmers. The security model ð the most abstract view of the system ð is claimed to be ðapplication-basedð, in that the designers found out what the problem was first, and then constructed the model. Intuitive understanding of what ðsecurityð meant was formalised by considering the application domain. The example model is a non- deterministic state machine, with classified ðentitiesð which may contain each other. The definition of security in this model is a predicate on the histories of the system. The next stage in the methodology is the decomposition of the system into modules. Each module specification consists of several documents, including an Access Program Table, which gives details of the moduleðs interface as a reference for programmers. The semantics of the calls (and their exceptions) are in English for most modules, but have been formalised for the ðEntity Moduleð. Module specifications must be interpreted in the language of the security model. Only the Entity Module has a formal interpretation of this sort, in which the module is interpreted as a complete system, although the formal interpretation used could be applied to other modules. There is no discussion of why each individual module needs the security properties of the whole system, of how modules are composed, or of why composition should preserve security. The security of a module specification is defined to be the security of the interpretation of the module specification in terms of the abstract security model. This proof of security is reduced to showing that a security invariant is preserved by each call to the module; the security invariant must be shown to imply the weakest precondition of the call, with respect to the invariant as postcondition. This is a weak link in the methodology ð the ðweakest preconditionsð used are informally derived (and sometimes not even equivalent to the call semantics), which could be dangerous in more complex specifications. Inspection of why preliminary proofs fail guides the improvement of the module specifications ð the process iterates until the proof of security succeeds. Proofs were performed by hand. Overall, this methodology aims to obtain benefits quickly by using a semi-formal approach, rather than use a high-cost, fully rigorous methodology. (In practice, subtle design flaws were uncovered by the failure of semi-formal proofs). Unfortunately, there are many crucial steps whose soundness is not built in to the methodology, but must be checked by hand for every application. Also, only two levels of abstraction are catered for (model and specification), which would limit the applicability of the approach. However, this paper details some very useful experience, gained the hard way over a long period of time, and could in principle form the basis of a rigorous, machine- supported development methodology. #ABSTRACT#164# Note: This paper discussed how a multi-level replicated database my execute a user's transactions in the order of submission, without interference from other database commands issued by other users. #ABSTRACT#165# This paper is mainly about the ways of providing backup computing facility if the main facility is lost for some reason. It is relevant to large system DP management. #ABSTRACT#166# A progress report on the 'Euclid based Verification and Evaluation System' (EVES) and the Ottawa Euclid compiler. This paper contains some rather worrying assertions about the lack of a sound theoretical basis for mechanical verification systems. #ABSTRACT#167# The procurement option of using an untrusted DBMS on a TCB where both trusted system and DBMS functionality is required is briefly discussed in appendix B of the Trusted Database Interpretation. This paper discusses an approach proposed for a Canadian Department of National Defence project to design and implement several multilevel multiuser DBMS-based applications using a trusted DBMS on a B1 UNIX TCB, and the design and operational constraints imposed by this solution. #ABSTRACT#168# Note: This paper takes a paper microprocessor - the FM8501 - and verifies the correspondence between the machine code and the microcode. The machine was originally designed by Hunt to demonstrate the use of Boyer-Moore in microprocessor verification. This work uses an alternative proof system, the State Delta Verification System, to repeat Hunt's work and show equivalence between the two methods. The main conclusion is that verification of paper machines is possible today, but that further work is required to address real systems. This unsurprising result is in line with that for verification systems outside the specialised field of microprocessor verification. It is worth noting that some work on specifying real microprocessor instructions sets in Z has been done in the UK and the precondition / environment / postcondition style used here has its similarities to Z. The FM8501 microprocessor was defined and verified by Hunt in 1985 using the Boyer-Moore theorem prover. A reverification of the same machine using the State Delta Verification System has been carried out. This work correlates strongly with work done by Hunt, demonstrating that the verification community is capable of supporting its own results, drawing on the diversification of proof tools to provide independent validation of previous work. The proof strategies and the complexities that are encountered in proving correctness of microcoded processors are discussed. #ABSTRACT#169# Note: This paper is a proposal for experimental work to determine the feasibility of a virus (and Trojan Horse) filter program. A virus filter is defined as an analysis program that is capable of sorting ðclearly OKð programs from ðnot clearly OKð. The approach being considered is the formulation of a limited specification (restriction) for programs which details the modifications that it can potentially make both to external objects and to itself by dynamic code generation. Furthermore, the policy of the system with respect to such modifications is to be formulated and applied to each program in conjunction with the program-dependent restrictions. The intention is to be ðsafeð with respect to virus detection, the almost inevitable price being paid is that some programs which are actually OK would be rejected by the filter. The filter is also intended to be used in a ðnormalð system environment such as MS/DOS or UNIX. The method proposed rests on three stated hypotheses: „ that the majority of useful programs are amenable to the formulation of syntactically simple hypotheses; „ on average, benign programs are simply analysable; „ modifications are classifiable into ordinary and suspicious categories. It is hoped that the experimentation with the above-named operating systems will determine the viability of the first and last of these hypotheses. On the face of it, the second hypothesis appears reasonable as it stands. The approach shows some promise and the results of the investigation may well be worth following. #ABSTRACT#170# The vast range of security levels/compartments, complex ownership, continuous evolution, adaptive policy requirements, and large size of battle management systems (BMS) make it evident that the trust issues are substantial and will require extensive attention throughout the development cycle. This paper outlines the software development process and identifies where trusted system development requirements fit into the process. The main contribution of the paper is the identification and discussion of eight leverage points that cut across the entire development process and provide the greatest opportunity to affect the security of the software that is developed. #ABSTRACT#171# The SRI Verification System is an interactive system for the composition and analysis of formal specifications and abstract programs. Until something better is agreed on the system is known as 'Enhanced HDM' and its specification language as 'Revised Special'. This document concentrates on the verification system - it tells you what facilities are available and how to invoke them. It also explains some of the theory behind the theorem prover provided in the system since this information is not readily available elsewhere. The companion document describing the Revised SPECIAL specification language in detail is an essential adjunct to this one. #ABSTRACT#172# A preliminary definition of the specification language. The language, provisionally designated 'Revised Special', is intended as a successor to both the language of the STP verification system and HDM/SPECIAL. #ABSTRACT#173# Note: EHDM is a specification and verification environment which is hierarchical both in terms of modules and in terms of abstraction. It consists of a specification language (largely based on typed first-order predicate calculus, but also including elements of richer logics such as higher-order logic, lambda calculus and Hoare logic), and an environmental tool-kit including a theorem prover supporting both automated and interactive proof techniques, and a 'multilevel security tool', which analyses specifications for compliance with a (non- interference-style) multilevel security model. It does not provide or support a programming language, but instead offers procedural constructs at a level of detail similar to that found in Ada or Pascal; within the environment there is a tool to translate imperative code- level specifications from EHDM into executable Ada code. It is expected that the formal semantics of the EHDM specification language, and a rigorous description of the operations implemented in the EHDM environment, will be completed in 1989. #ABSTRACT#174# The VIPER 32-bit microprocessor has been invented at the UK Royal Signals and Radar Establishment (RSRE) for use in highly safety- critical military and civil systems. Throughout, formal mathematical methods have been used to prove that the gate-level realisations conform to a top-level specification. The paper explains the various layers of documentation produced, starting with the use of LCF-LSM (based on Meta-Language, ML) at the higher levels, proceeding via the use of ELLA hardware description language at lower levels, to multiple VLSI implementations . It is intended to show that this route for designing synchronous VLSI circuits promises a practical means for industry to produce validated designs. Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188) #ABSTRACT#175# It has been recognised that available workstations could significantly enhance the capabilities of today's Intelligence Data Handling Systems (IDHS) if they could be integrated with the IDHS systems in a secure manner. The Compartmented Mode Workstation (CMW) project was started to further the state-of-the-art of computer security in general and workstation security in particular. The prototype effort had two major purposes: to demonstrate that operationally useful implementations of each requirement could be designed and developed, and to gain insight into what measures could be taken to augment commercially available workstations with meaningful security. This paper describes compartmented mode operation, how the prototype satisfied each requirement, and the level of effort involved in the prototype implementation. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 2 - 12 This is an account of modifications required to a workstation software and firmware, to provide a form of mandatory access control which supports 'compartmented mode' working while allowing off-the-shelf application software to be used. Unfortunately, a full description of compartmented mode security is not given in the paper, despite the authors' insistence that the reader must understand exactly what is meant by CM operation. Doubtless a complete description is available through the referenced official sources. From the presentation (not the paper) it was gathered that CM operation implies: „ one or more multilevel secure hosts storing a wide variety of classified information „ workstations each dedicated to a particular security compartment, and within that offering multilevel security/mandatory access control. Users permitted to log on only at specific workstations „ a CM net which permits one-way flow of information from host to workstation, filtered according to compartment of workstation. Data is prepared on the workstation and released from the workstation. The bulk of the paper describes changes to Unix for security and the privilege system. #ABSTRACT#176# In reasoning about policy based on information flow control, we can adopt two different points of view de- pending on whether we deal with explicit permissions or explicit prohibitions. In both cases, we use an epistemic and deontic logic to formally define information a subject is permitted to know. Then, we show how the causality property [2] can be derived from the explicit permissions point of view and how the non- interference [5] and non-deducibility [11] properties can be derived from the explicit prohibition point of view. However, we argue that the prohibitions enforced by non-interference or non-deducibility are generally too rigid and leads to too strong security properties. On the other hand, the causality property only han- dles internal information flow controls and it must be completed to ensure that the security policy is consis- tently defined. Hence, the consistency problem is dis- cussed; we propose a general definition and practical conditions to verify that a security policy is consistent. We think that the policy consistency problem is closely related to the so-called inference problem in multilevel databases. #ABSTRACT#177# In this paper, we show that the analysis of functional dependencies is very useful when we want to decompose a multi-level relation in a collection of single-level relations. We study the decomposition of a multi-level relation into a collection of 4NF relations according to various functional dependencies. These decompositions are compared to the decomposition algorithms in single-level relations proposed by SeaView) and by Jajodia-Sandhu. It appears that the first step of these decomposition algorithms is simply the normalization of the multi- level relation in 3NF (or in 4NF). Then, we propose an analysis of functional dependencies which seems natural from a semantical point of view. We decompose a multi-level relation into 4NF relations according to these functional dependencies and we should then how to decompose these relations into single-level relations. We think that this analysis provides a good solution to the polyinstantiation problem and that it would lead to correct definitions of update operations. #ABSTRACT#178# NewSpeak is a language designed for use in safety-critical programs. It tries to limit the freedom of the programmer to the kind of ideas in programming that are reasonably easy to formalise without making these restrictions unduly onerous. Its principal characteristic is that it has no exceptional values or states. Incorrect constructions which would lead to exceptional behaviour such as range violations or numerical overflow, are all dealt with at compile time. Initially intended for use on the VIPER processor but it is not limited to the VIPER. #ABSTRACT#179# Note: This paper describes the mappings between the various stages of product development (from requirements to hardware via software) in terms of translations of both into state deltas, using the State Delta Verification System (SDVS). The necessary conditions are that the mappings between the various stages are sets of ordered pairs of models; in each pair, the time-line of the upper-level model is a subset of the time-line of the lower-level model; and for a given mapping, two predicates correspond at their respective levels if and only if for all implementations, the lower-level predicate in the lower-level model implies the upper-level predicate in the upper-level model. It is also necessary for the time-lines to correspond and (in the SDVS system as it stands) for the upper-level predicate to be expressible in the lower- level logic. #ABSTRACT#180# Note: This book is the standard reference for IBM's System Network Architecture system of protocols. Unfortunately it is currently out of print. #ABSTRACT#181# This paper presents an overview of the initial application of a risk- driven reasoning-based development paradigm to a trusted X Window system prototype on Trusted Mach. The goal of the prototype is to evolve to a system that, after refinements, will be certifiable at a B3 level of trust. The paper provides a snapshot of current research work in progress. It focuses on tailoring of the development paradigm based on the risk identification and mitigation performed early on the project. Actual project results in terms of the major risk mitigation activities of the first two spirals are presented. The difficult issues involved in stretching trusted system technology on several fronts (complex system application, new development approach, and lack of TCSEC interpretation for windowing systems) are stressed. The paper concludes with some general observations and initial lessons learned about our application of the development paradigm. #ABSTRACT#182# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#183# An 8-page review of UNIX 5.0, its position on the market and its security features. In essence, it has no mandatory security but good password protection and owner/group/other discretionary security on files. Its NCSC rating would be probably C1 or C2. The review explains why this version of UNIX is likely to become dominant and why UNIX itself is likely to become dominant. #ABSTRACT#184# This report looks at the need for identification of people by their personal characteristics rather than by transferrable items - passwords, keys etc. It then looks at the existing commercially available products, which can be categorised by the method used: fingerprint scan, retinal scan, voice analysis, hand geometry scan and signature dynamics analysis. Most products are designed for physical access control, though the technologies should be applicable to computer access control. The report ends with a comparison of the products in tabular form. (Update of December 1986.) #ABSTRACT#185# Honeywell Bull's Multics operating system is generally considered the most secure general-purpose operating system now available - the highest rated large-scale system evaluated thus far by the National Computer Security Center (NCSC). Multics is a large-scale, multipurpose, virtual memory computer operating system designed to support 40 to 400 concurrent users in a highly secure, interactive environment. A three-dimensional data security policy, enforced in hardware, is an integral part of the system. #ABSTRACT#186# General Comprehensive Operating Supervisor 8 (GCOS 8) from Honeywell Bull Inc (formerly Honeywell Information Systems Inc) is a flexible, user-defined, user-oriented virtual operating system capable of batch, time-sharing, and transaction processing. In addition, GCOS 8 offers software security through passwords and a File Management Supervisor (FMS) along with hardware safeguards through controlling access to sets of memory segments called domains. #ABSTRACT#187# This Datapro report is based on a paper presented to the IEEE 1986 Oakland Symposium by Leslie Chalmers. #ABSTRACT#188# This loose-leaf, 3-volume publication on information security consists of a series of reports on a variety of topics (many of them reprints from technical journals, others specially written), including surveys of available hardware and software. It is updated monthly. #ABSTRACT#189# This report is a summary of the security features by the VMS operating system for DEC VAX computers. (Update of Feb 1988) #ABSTRACT#190# Note: This report compares and contrasts the main access control add- ons available for IBM MVS systems: RACF, CA-ACF2 and CA-Top Secret. #ABSTRACT#191# An overview and analysis of RACF, IBM's offering giving added security to their operating system MVS. This product is currently rated C1, but is being revised to C2. #ABSTRACT#192# Infosafe Corporation, Formerly A-O Electronics, manufactures a family of microcomputer encryption and access control products called X-Lock. All products in the X-Lock family protect information stored on IBM and compatible microcomputers by limiting access to the computer's hard disk and encryption of sensitive information. The X-Lock 10 is Infosafe's entry-level product, offering the buyer of security of hardware-based start protection without requiring the purchase of features that may not be required. The X-Lock 10's modular design permits the buyer to purchase directory control, Data Encryption Standard (DES) encryption, program authentication, and audit trail capabilities. X-Lock 10's strengths lie in its hardware-based protection, familiar user interface, and virus protection capabilities; however, its other capabilities are those of a more basic security product. In addition to competing with the X-Lock 50 and 100 products produced by InfoSafe, X-Lock10 competes with established products such as Watchdog from Fischer International, OnGuard from United Software Security, and Protec from Sophco, Inc. InfoSafe was originally established as A-O Electronics in 1985 to manufacture custom voice communications encryption devices. A shift in the company's emphasis to personal computer data security products resulted in a name change to InfoSafe Corporation in 1988. #ABSTRACT#193# Note: This report is based on the paper with the same title presented by M Satyanarayanan at the 11th NCSC,October 1988. #ABSTRACT#194# Note: Also published by Purdue State University as CSD-TR-933. #ABSTRACT#195# Note: Based on NCSC A Guide to Understanding Design Documentation in Trusted Systems, NCSC-TG-007, Version V-1, October 2, 1988. Design Documentation is a TCSEC requirement for classes C1 and above. The purpose of this report is to provide developers of trusted computer systems with guidance in understanding and meeting the design documentation requirements contained in the TCSEC. To accomplish this , the report addresses two goals. First, the report increases the vendors' awareness of the importance of design documentation to the security of their system throughout the system life cycle. Second, the report forms an initial basis of understanding between the vendor and evaluator communities concerning what is expected by the evaluation team in the review process and deliverables for design documentation. #ABSTRACT#196# This report, written for Datapro by Honeywell, gives a readable description of the history of Scomp development to June 1985. It describes the basic security mechanisms and the hardware and also the kernel, the trusted software and the interface package, SKIP. #ABSTRACT#197# Summarises the security features of the Honeywell Multics, the first - and so far (1986) only - operating system to achieve the TCSEC B2 rating (September 1985). Multics runs on a special version of a Honeywell 36-bit mainframe, scheduled to be phased out in 1988. Multics has three independent mechanisms: a seven-layer hardware 'ring' to protect the operating system and user subsystems from user modification; an ACL system to provide discretionary security; and an Access Isolation Mechanism (AIM) for non-discretionary security. The latter two are software managed but hardware checked, via capabilities, thus providing assurance and efficiency. #ABSTRACT#198# MVS is IBM's preferred operating system for its larger mainframes, often run under the VM operating system. It is not itself undergoing evaluation, but access control packages are available that have been, namely ACF/2/MVS (C2), CA-Top Secret (C2) and IBM's own RACF (C1, being re-evaluated against C2) #ABSTRACT#199# The AOS/VS Operating System for Data General Eclipse/MV minicomputers is described. This product is being evaluated by the NCSC and recent changes to the product are believed to be in support of a C2 rating. #ABSTRACT#200# A very superficial look at the role of tiger teams in establishing security weaknesses; mention is made of the use of this technique in 1973 against a Pentagon computer, which eventually led to the formation of the ADPSSD team that tests the US DOD computers handling classified information. #ABSTRACT#201# Note: This report describes the security concepts and administration aids in the UNIX operating system. #ABSTRACT#202# VMSecure is an access control, disc space management and data encryption package for IBM computers running the VM operating system. It was being evaluated at level C2 by the NCSC, but the process broke down over NCSC requests for changes to the product. #ABSTRACT#203# Note: Throughout this paper a strong analogy was drawn between the problems facing software vendors and their clients and the problems facing the pharmaceuticals industry and consumers in the current climate of increasing consumer terrorism. The latter attempts to counter the possibility of unauthorised modification of the product via the use of tamper-resistant packaging. The basic assumption is that the software is produced in a clean environment, and the problem tackled is that of unauthorised modification post-release. The method used is essentially that of appending a signature to the product the authenticity of which is enforced by cryptographic sealing using a public key cryptosystem. Furthermore the software is to be protected while in the usersð environments against modification and backtrack attacks. It is recommended that although the vendorðs authentication device can be in software, the security-conscious user should employ a stand- alone hardware authenticator to avoid the problems associated with the necessary protocols involved with using a software authenticator. It seems that special architectural support in the userðs system may be necessary. It is also recommended that authentication be possible while a program is executing since swapped-out processes are vulnerable to virus infection while they are in memory. This involves signatures being placed in the software at the block or even instruction level. This may require changes to the user systemðs memory manager, for example. It is also possible that a stand-alone authenticator could check the operating system itself at random times. #ABSTRACT#204# This is a comprehensive, easy to read practical guide to many aspects of computer networks from the concept of packet switching to the terminals used in the network. It covers the common protocol issues, such as routing, flow control and congestion avoidance, and packet broadcast systems in separate chapters, leaving high level protocols (the OSI transport layer and above) to a single chapter on its own. Examples are taken from ARPANET and other established sources of experience with little reference to the, more abstract, work that ISO has done. The chapter on communication protocols gives an insight into their implementation and design. It deals with X.25 and its supporting layers (HDLC in particular) which it considers in detail. Indeed, in general, everything mentioned in the book is given a comprehensive exposition. There is a brief but informative chapter on message authentication and the book concludes with one about network optimization. The lists of references at the end of each chapter are a useful basis for further exploration #ABSTRACT#205# This book looks at data security using cryptology; it does not go into topics such as access control. The book starts by giving a quick look at various historic encipherment methods such as the Vigenere cipher and the Enigma machine. The DES algorithm is described in detail, not just the mechanics but the history, its security, and various implementations. Various one-way and 'authenticator' ciphers are discussed. A interesting chapter on key distribution describes key generation, a session key distribution protocol, and the IBM key management scheme for file security. The chapter on user identification describes in detail and assesses many of the currently employed techniques. Other chapters cover Public Key systems (including RSA), digital signatures and EFT (including SWIFT and the use of smart cards). #ABSTRACT#206# Note: This paper characterises two different forms of virus: „ The 'patch' approach, in which a jump instruction is patched into the code, and additional code is appended to the original, to perform the viral action. These viruses may preserve the original functionality of the code, and so may escape immediate detection, but they can be detected by changes in the length of the executable file. „ The 'overwrite' approach, in which a section, or all of an executable is overwritten by some viral code which may or may not destroy the original functionality. These may be combatted by keeping tables of checksums. The speaker proposes that, to maintain the integrity of a networked filestore, it may be necessary to dedicate a workstation on the network to repeatedly checking the network filestore for viral infection, using known good checksums. The paper gives a number of examples of program code suitable for performing this form of check The presentation appeared to be not inspired, but competent. #ABSTRACT#207# Network users may be authenticated by different means and from a variety of locations. Once authenticated, the user's access should be consistent with the strength of the authentication. This paper examines one possible method for determining the authentication strength and conveying this information within a distributed network. The approach discussed uses a token composed of a unique user ID and an authentication level. The token is sent along with the request for establishing a remote session. Once the token is received, the remote location determines user access based solely on the authentication token. #ABSTRACT#208# This paper boils down much of the existing virus research into a succinct set of inference rules. These rules are then expanded to include the newer self encrypting stealth viruses along with the necessary conditions for their detection. This foundation is then applied to derive additional properties of new viruses. #ABSTRACT#209# This paper describes a software program used for identifying the executable software configuration installed on a computer. The application, "Auditor's Aid", allows an auditor to automatically identify what programs (and versions) reside on a given system. The approach discussed generates a checksum and uses this value as a primary key (not to be confused with an encryption key) into a configuration table. The prototype described operates on an IBM PC platform. #ABSTRACT#210# As computer science advances at a prodigious rate, its application in many fields is introducing sweeping change at a similar rate. A significant issue generated by this phenomenon is the security of information in digital form. This issue is concerned not only with military security but also with the protection of sensitive, unclassified industrial information. This paper focuses on the latter type of data protection. It suggests common descriptors of data protection and information security applicable to security of digital information which is entitled Electronic Information Security (ELINFOSEC). #ABSTRACT#211# Superceded by report TXSG-87-19, An annotated bibliography on computer security. #ABSTRACT#212# Superseded by TXSG-87-8, Lattices for computer security #ABSTRACT#213# This paper presents the mathematical definitions leading up to the concept of a lattice, and then presents and proves various properties about lattices that make the concept useful in the field of computer security. #ABSTRACT#214# This has been superceded by TXSG-87-8, Lattices for computer security #ABSTRACT#215# Note: This paper looks at various subsystems and considers whether they conform to the idea of a component as the term is used inside the TNI of the TCSEC. #ABSTRACT#216# In this paper, we present a possible application of neural networks as a component of an intrusion detection system. Neural network algorithms are emerging nowadays as a new artificial intelligence technique that can be applied to real-life problems. We present an approach of user behaviour modeling that takes advantage of the properties of neural algorithms and display results obtained on preliminary testing of our approach. #ABSTRACT#217# An interesting book consisting of a number of significant papers on many aspects of the subject. #ABSTRACT#218# This paper introduces some of the problems discussed in subsequent papers in the same book, in particular access control mechanisms such as the take-grant model, and statistical inference on the results of interrogating a database. #ABSTRACT#219# The security of Multilevel database systems is threatened in a number of ways. In previous work Denning showed how trusted filters and cryptographic sealing can be used to prevent some of these threats. In this paper she shows how a commutative filter can be used to stop leakage via inference and Trojan horse. The filter can be applied to the database so that the DBMS only acts on an authorised view, or it can be applied with the same effect to the results returned by the DBMS in response to queries. This means that the DBMS can perform the query selections, query optimisation and (some) projections, reducing the work required by the trusted filter #ABSTRACT#220# The first half of the book is devoted to cryptography, starting with the general principles and some mathematics, then describing some encryption schemes (including DES and RSA), and then giving ways in which encryption can be used in computer systems such as signatures, logon protocols and key distribution. The second half of the book is concerned with access controls, information flow and inference, and describes many of the problems in this area. A detailed treatment of a number of formal security models is given. #ABSTRACT#221# A tutorial on some of the privacy and protection issues for databases. It aims to be useful both to technical and non-technical audiences. Topics covered included a description of the protection methods in the IBM relational database package SQL, and how encryption could be used for protection of multilevel data. #ABSTRACT#222# The paper presents a draft model for IDES, an Intrusion Detection Expert System, which is based on the premise that to expolit weaknesses the system has to be used in an 'abnormal' way, and, if all actions were monitored , an expert system could detect this abnormality. The expert system consists of an audit analyser which is driven from a database of rules; audit event records are processed using pattern- matching techniques, and then compared against activity profiles stored for each user. Anomalous events which cannot be handled by the rules are passed up to a human authority. This gives a useful combination of automatic and manual control. It appears that the code can be implemented in a system independent way, dependencies being confined to the rule database. Also, if the rules are expressed in a system independent way, there is a possibility of exchange of rule information between different systems, thus placing less reliance on the skill of site security officers to formulate rules. The major question is whether the rules can be set so as to avoid major loopholes while keeping a reasonably low rate of events passed up to the human controller. At present (1986), the work is purely theoretical. #ABSTRACT#223# This paper presents a formal security model based on information flow. Information flow models are concerned with the flow of data between objects, either directly, or indirectly by derivation. Both the objects and the subject, the active agent responsible for data flow, have a security class associated with them. Denning shows that valid information flow can be used as the ordering relation on the set of security classes and that under this relation the security classes form a lattice. Hence maintaining secure information flow in the system corresponds to ensuring that actual information flows conform to the lattice. Denning states that the main problem with guaranteeing security is in detecting the information flows, especially implicit flow, when the information in one object is used to derive the information to be transferred to a second object. The paper presents a set of conditions under which a sequence of statements causing both implicit and explicit flows are secure. #ABSTRACT#224# Denning looks at the problem of allowing statistical queries of a database while avoiding compromise of data on individuals. A basic technique is to reject queries revealing information about small groups; Denning extends Freidman and Hoffman's idea of implied queries, but shows that the work required increases exponentially with query order (number of attributes concerned), and so we have to fall back on Beck's data perturbation scheme or Denning's Random Sample queries #ABSTRACT#225# This paper summarises the papers that show how to compromise databases that tell the truth, even if they refuse to give information about small samples. It points out that any stochastic perturbation of the results can be filtered out using communication theory techniques, so pseudo-random rounding is better than truly random rounding. #ABSTRACT#226# This paper proposes a method for using encryption for protection on a network used for personal computing. the scheme uses a public-key encryption device in the network interface, with the secret keys built in to a key card or similar. As well as protecting personal data in transit and while stored in a central facility, it also protects against thefts by trojan horses in 'public' software except by use of covert channels. Data sharing is done by duplicating under the other parties' public key, and the scheme can be adapted for digital signatures. #ABSTRACT#227# The aim of the work underlying the paper is to design a MLS/DBMS based on protected views using relational model. The paper describes views and summarises the motivation for using them. Classification can be attached to views and then these act as rules for adding classification information when updating the database. There is a significant problem in ensuring this labelling technique is complete and consistent. The paper also discusses how views can be used to control aggregation, and ends with a sketch of a tentative design for a system that is hoped to be A1 secure. #ABSTRACT#228# How to do compile time information flow analysis. #ABSTRACT#229# Note: This was one of two papers at the symposium from SRI and Gemini, on the Seaview multilevel secure relational database project. This paper presents a security policy model. The information is presented at a point in the project where specification and design are substantially complete, although implementation has not started. A most interesting feature is the separation into two models in adjacent layers. The innermost layer, called the MAC model, deals with mandatory security. It is an extension of Bell/LaPadula with an integrity component. Since the interpretation of Bell/LaPadula objects is as single-level database relations, a general-purpose commercially available A1 security-kernel can be used to implement the MAC model. The second layer of the model is called the TCB, and describes security in terms of relational database concepts. This accounts for the bulk of the paper. nineteenð(!) properties are defined. Property 1, for example, is that the class of tuple dominates the class of every element in it. Although the requirements for mandatory security are handled entirely by the MAC model, the TCB model which sits on top of it is greatly influenced by the requirements for the MAC model. A formal security policy model that uses basic view concepts for a secure multilevel relational database system is described. The model is formulated in two layers, one corresponding to a security kernel or reference monitor that enforces mandatory security, and the second defining multilevel relations and formalizing policies for labeling new and derived data, data consistency, discretionary security, and transaction consistency. This includes the policies for sanitization, aggregation, and downgrading. The model also defines application- independent properties for entity integrity, referential integrity, and polyinstantiation integrity. #ABSTRACT#230# Note: Prepared for Rome Air Development Center, Griffiss Air Force Base, NY 13441-5700. #ABSTRACT#231# The report describes a proposed system which is potentially very good. The report is quite readable, especially Chapters 5 on, which give a good summary. Unfortunately, as far as can be gathered, the work is entirely theoretical at present. The 'expert' in the expert system of the title refers to a system driven by a database of rules. The rules are partly suggested in the report and will be partly contributed in a working system by the security officer (or committee). Events which cannot be coped with by the rules are passed up to a human authority. This gives a useful combination of automatic and manual control. It appears that the code can be implemented in a system independent way, dependencies being confined to the rule database. Also, if the rules are expressed in a system independent way, there is a possibility of exchange of rule information between different systems. The major question is whether the rules can be set so as to avoid major loopholes while keeping a reasonably low rate of events passed up to the human controller. A reduced version of this report appeared as a paper: D.E. Denning, 'An intrusion detection model', Proc. IEEE 1986 Symp. Security and Privacy pp. 118-133. #ABSTRACT#232# Note: Also available in Turn, Rein: Advances in Computer System Security, Volume III, #ABSTRACT#234# This paper show how the Needham-Schroeder key distribution algorithms can be adapted by using timestamps to protect against replay, and also to protect against impersonation should a conversation key be compromised. It requires each endsystem to maintain a clock accurate to, say, the nearest minute, and also stops the key renewal mechanism used in the Birrell protocol. #ABSTRACT#235# This paper describes practical models used to conduct threat and risk analyses for large information systems or networks. The process of analyzing and relating threat agents, assets, and safeguards within a static threat model is described. In addition, a dynamic risk model is described that consists of threat events, security failures, and damaging outcomes. This approach permits the incorporation of known baseline security requirements such as policies and standards, as well as hardware and software security features that could be distributed throughout the information system. #ABSTRACT#236# An intrusion-tolerant distributed system is a system which is designed so that any intrusion into a part of the system will not endanger confidentiality, integrity and availability. This approach is suitable for distributed systems, because distribution enables isolation of elements so that an intrusion gives physical access to only a part of the system. By intrusion, we mean not only computer break-ins by non- registered people, but also attempts by registered users to exceed or to abuse their privileges. In particular, possible malice of security administrators is taken into account. This paper describes how some functions of distributed systems can be designed to tolerate intrusions, in particular security functions such as user authentication and authorization, and application functions such as file management. #ABSTRACT#237# In dynamic circuit design many rules must be followed which govern the correctness of the design. In this paper a dynamic CMOS design style using a two phase non-overlapping clock with its intricate design rules is presented together with formal means of showing that a circuit follows these rules. #ABSTRACT#238# Note: PhD Thesis. #ABSTRACT#239# Encryption algorithms are vulnerable to exhaustive searching for the key: if an enemy has the plain text and corresponding cipher text it is possible to try all of the possible keys in turn until the correct one is found. This paper describes the application of this technique to the NBS (now usually known as DES) algorithm. It is shown that the algorithm is vulnerable to this sort of attack, but in practice only if the key searching is done by many DES devices working in parallel, with each device searching a different part of the key domain. The design of a hypothetical machine constructed for this purpose containing one million DES devices is considered in detail. With such a machine the average time to discover a key would be ten hours. This article subsequently led to much speculation about the adequacy, or otherwise, of the DES algorithm. #ABSTRACT#240# This paper describes the important cryptographic algorithms which had been and were being developed in 1976. It has an introduction in which the problems are usefully and clearly stated. It forms a useful survey of design techniques without going into the mathematics at any great depth. #ABSTRACT#241# Note: The aim of the project discussed here is an internet system ('Multinet Gateway System') with an A1 security certification; the system consists of a set of networks linked by gateways forming a transport service. The major problems are those of fragmentation and repetition of data, and there is no guarantee of delivery; denial of service is not addressed in this paper. A question was asked about how the interfaces ensure that 'information' and 'non-information' data are not mixed . The reply: 'See Dinolt's paper in IEEE 1989'. #ABSTRACT#242# KSOS extends Bell-Lapadula to have integrity levels as well as security levels; this paper extends the KSOS model to an object/object model called CPM. Each object has 3 pairs of security and integrity levels: migration, absolute and corruption. Migration levels specify the highest security level (MSL) and lowest integrity level (MIL) to which data migh flow; absolute levels (ASL, AIL) classify the data in the object, and corruption levels (CSL, CIL) specify the levels from which data can flow into the object. For each object, MSL>=ASL>=CSL and MIL<=AIL<=CIL. In a similar way, users (subjects) have associated read, absolute and write levels for security and integrity. The paper describes how the levels of a subject and two objects can be used to check whether a connection can be established by the subject between the objects, and then mentions some examples of the use of CPM. #ABSTRACT#243# Although this report is currently in flux it does represent an attempt to provide a framework for the standardisation of distributed services, such as message handling services (as already represented by X.400), directory services (e.g. ECMA TR/32), filing and retrieval, printing and the general field of security. This version of the document is due to be replaced by an enhanced one. The document introduces a number of basic concepts including the client/service model, categorises different kinds of service, and lists a number of requirements. It defines four primary 'productive services' (mail, mailbox, filing and printing) and four 'supportive services' (time, authentication, directory, bulk data transfer), and outlines the way in which the productive services are supported and the way all the services interact with each other and with a user. There is a chapter outlining many security concepts for distributed services, and for an authentication service and access control in particular, and there is a discussion of naming. Finally a number of guidelines for the design of access protocols for distributed services are presented. #ABSTRACT#244# Note: The paper describes a front end to the Gypsy Verification Environment (GVE) which is intended to increase the proportion of proofs which can be carried out automatically. The front end is a ðknowledge-based tool to aid in organising knowledge and strategies for performing proofs using the GVEð. The front end is called the Deductive Theory Manager. Contrary to my expectations, the word ðtheoryð occurs nowhere in the text of the paper except in repetitions of the title. The knowledge base consists of a tree, or ðstrict hierarchyð, of ðobjectsð. These objects contain ðproof expertiseð and correspond more or less to what we would call tactics; programs in the form of ðscriptsð and ðrulesð for deciding what GVE command to issue next in the light of the given proof-goal. The organising principle for the tree is: the more general the expertise the closer to the root, and the more specific to the application, the further away from the root. This means, I think, that the organisation of the tree is not a reflection of the structure of any particular proof. Nor is it exactly the structure induced by the relation of parenthood between one theory and another, because any object in the tree has at most one more general immediate parent object. We are more used to a system whereby a given theory may be descended from several independent theories (although all ultimately have a common ancestor). Thus it appears that the knowledge base is a tree of tactics, which corresponds only informally to a structure of theories. Thus, to work on a particular proof goal, the user selects a script, which is some point in the tree. If all the rules fail at that point, the system tries the (one and only) immediate parent script in the hope that more general rules will be applicable. This effort is motivated by the large amount of work necessary in the verification tasks undertaken by the authorsð organisation. For one effort, FTLS-to-model verification for the kernel of a secure operating system called ASOS, there are 461 independently proved lemmas which would amount to 7600 pages of formatted Gypsy proof-logs. The large number of lemmas arises from effort to decompose and modularise the proof effort. The goal of the DTM is to capitalise on the similarity within groups of proofs induced by a uniform writing style for specifications and the decomposition into many lemmas. The work is not complete, and no assessment of the effectiveness of the DTM is given. Formal verification tools and techniques are difficult and expensive to apply. To make verification of large, complex systems more practically feasible, TRW is developing the Deductive Theory Manager (DTM). A knowledge based tools that integrates with the Gypsy Verification Environment (GVE), the DTM supports the construction of deductive theories and applies them to proofs. Knowledge bases applicable to a variety of projects, and one specific to the Army Secure Operating System (ASOS) proofs, are simultaneously under development. This work derives from a previous effort headed by Ben diVito. This paper describes the underlying philosphy of verification strategy on which the DTM is based, presents the DTM architecture, and illustrates DTM knowledge engineering and proof processing with a case study. It is assumed the reader is familiar with the basic concepts of formal verification and the Gypsy Verification Environment. #ABSTRACT#245# Note: This paper looked at a specific aspect of the immediately- preceding paper on the Army Secure Operating System, concentrating on the approach taken to verifying the multilevel secure kernel. The design used two different notions of state, at the model layer and at the FTLS layer. At the model layer, there is the protection state, an abstract Bell-LaPadula-based representation of the protection-critical aspects of the reference monitor. The FTLS kernel state includes nearly all aspects of the kernel, in a level of detail very close to a full implementation. An interpretation function, formalised using Gypsy, maps from the more detailed to the more abstract representation and provides a way of determining the effects of ASOS kernel services on the security model properties. To demonstrate that the system is secure, it was first demonstrated that the initial state of the kernel satisfied the security properties, and that each kernel call, represented by a procedure declaration, was security preserving. By modelling the idealised machine as a Gypsy program which calls procedures representing kernel calls, the Gypsy Verification Environment could be used to generate the verification conditions to be satisfied. There were about 90 different transitions of the kernel state to consider, of which 20% caused no change in the kernel state (and so could not caused a change in the interpreted state); 50% caused a state change in the kernel state, but caused no change in the corresponding (via interpretation) protection state; and 30% which caused a change in both kernel and protection states. It was only the last category that need substantial effort to prove they are security- preserving. By adopting a systematic approach for each of the categories, it becomes easier to generate and review proofs. On average, the proofs consisted of 34 steps; lemmas were used to reduce the complexity of the longest proofs to about 100 steps. In all, proof documentation totalled about 18 MByte of data. The authors noted that whereas Gypsy was good for formal specification, GVE is difficult to use to prove security, and is weak in configuration control facilities. However, it proved worthwhile to produce some general-purpose lemmas early-on in the verification process, and also to do a few trial proofs before the FTLS is complete (as this may reveal ways in which the specification can be changed to aid the analysis). The style of specification adopted was chosen to enable both formal proofs of correctness and also machine analysis for covert channels; an unfortunate side-effect of the latter aim was that the FTLS was more detailed than it need otherwise be. One weakness with the approach described in the paper is that there is no formalised way of determining the correctness of the Interpretation Function. The Army Secure Operating System (ASOS) program, under the management of the U.S. Army CECOM organisation, is providing a family of operating systems of tatical data system applications in Ada. Two members of the ASOS family have been developed: a Dedicated Secure Operating System intended for the TCSEC [1] C2 level and a Multilevel Secure Operating system intended for the TCSEC A1 level. In this paper we present an overview of the A1 system concept and TRW's solution to the ASOS kernel verification problem. We describe the model, FTLS, and proff approaches as well as some practical techniques for coping with proof complexity. Summary statistics on the actual proofs have been compiled and included in our discussion of the verification results. #ABSTRACT#246# This paper shows how various problems in computer science can be considered subsets of a general problem of combinatorial inference, and proposes that this is a profitable new field of study. #ABSTRACT#247# Note: The talk was very well presented, which is also true of the paper. However, the content does not bear much relevance to the things the rest of the community are trying to achieve. Moreover, the authors appear to be trying to achieve too much because it looks as though they are developing a model which includes everything except the kitchen sink. One example of this is the section dealing with the concept of interpretation. The authors quite rightly point out that we should not be as concerned about information flowing as about meaning flowing. But to model the flow of meaning we need to model the knowledge of the recipient, an unrealistic task! Their work developed out of attempting to produce a security model for an IPSE. The authors noted that traditional security models, such as the Bell and LaPadula model, address secure systems as a product, but do not deal with the process of developing secure systems. Issues that need to be covered by such a development process are, for example, (i) the levels of trust assigned to tools, and (ii) information flows from development to target environments. Quite often there will be several different interests in a development, each having their own aims. These aims are set out as a policy. For example, one policy may be that the development is kept within costs, and another that it meets its functional specification. These policies sometimes conflict. The authors intend to model all these issues, and more. The key component of their model is the notion of a role. These reflect positions in an organisation and are things like technical authority and quality assurance. The roles fall into two categories, structural roles and functional roles. The structural role reflects the responsibilities and obligations placed on the role holder. The functional role reflects the actions of the role holder. Other components of the model are agents, actions and data. Agents cause things to happen and actions are the means by which this is done. Data is the means by which actions interact. The model sets out the complex relationship between these components. The paper finishes with a list of areas where the model would be, or is, useful. However, it remains to be seen if this is the case. #ABSTRACT#248# The paper examines the links between security and reliability, and argues that they can usefully be regarded as different aspects of a common problem and so amenable (at least in part) to common solutions. The paper suggests that an approach to system design that has fault tolerance as its aim can achieve both a high degree of security and of reliability. The requirements for a secure system and a reliable system can be stated in similar terms. The authors acknowledge that this sounds like playing with words, but state that this leads to an initial, but interesting, exploration of some of the parallels between security and reliability. The paper points out that work on security has concentrated on fault prevention rather than fault tolerance; it then investigates the advantages of using fault tolerance techniques to provide secure components from insecure components. As an example they discuss some of the drawbacks with the TCB approach to security, and illustrate how fault tolerance ideas could be used to circumvent some of these drawbacks. #ABSTRACT#249# Note: Supersedes CSC-STD-001-83. #ABSTRACT#250# A revised version of this manual was published in April 1978. #ABSTRACT#251# Superceded by later versions published irregularly by the US NCSC #ABSTRACT#252# This book defines the criteria for evaluating the security of computer systems set out by the US DoD Computer Security Center. It is essential reading for everyone in the field of computer security. It defines a series of categories each of which has a set of requirements. A computer system must fulfil all the requirements of a category to be approved in that category, and the requirements increase progressively in stringency. The criteria can be used to give a rating to the security properties of a computer system. These ratings are used in some US procurement requirements where there is a need to be able to handle classified material. The book is referred to as the TCSEC (and is also known as the 'orange book' due to the colour of the cover of the original document). #ABSTRACT#253# Note: This is a review of the covert channel threats present in LANs, based on a particular evaluation. Their conclusions may be arguable, but the paper contains an interesting collection of issues. #ABSTRACT#254# Today, the Department of Defense (DoD) relies upon software which would cost many billions of dollars to replace, yet many commands require the operational benefits of applied Multilevel Secure (MLS) technologies. Traditional secure engineering practices have started over again at ground zero and re-designed and re-engineered secure systems, creating whole new systems at substantial cost. We explore the idea of configuring a Trusted Computing Base (TCB) from commercially available components and porting existing software to the new environment with as few changes as is possible. When successfully applied, this approach can yield the DoD the benefits of applied MLS technology without incurring the costs and development time penalties associated with traditional secure systems development. #ABSTRACT#255# Note: This is a review of the article by Shannon published in Bell Technical Journal , Volume 27, 1948. #ABSTRACT#256# This book considers the security aspects of large mainframe systems. The first part is an overview of the components of a general system, and the security problems likely to occur in connection with each. The second part is a series of articles of experiences in particular large systems, from different manufacturers. The overview is quite short and simplified, but the practical articles give useful pointers to likely problems. #ABSTRACT#257# The requirements for multilevel security have been shown to conflict with some database integrity and consistency properties. In this paper, we examine the data consistency requirements for a distributed database system, consider the effects of multilevel security on meeting those requirements, and consider architectures for achieving them. We discuss the problem of providing serializability in a single- site database system and propose a solution based on optimistic concurrency control. We then extend this solution to a distributed database system. We also describe an approach for weak consistency concurrency control in a distributed database system based on the Optimistic Protocol. #ABSTRACT#258# The first part of the paper, presented by Debbie Downs, describes the purpose of Discretionary Access Controls (DAC), the lack of protection against Trojan Horses, some mechanisms that can be used to implement DAC - capabilities, user profiles, passwords, owner/group/world access bits and access control lists - together with their benefits and deficiencies, the access modes that are often found, and the relationship between DAC and file structure. As there is no formal model of DAC that fits myriad implementations, verifying DACs means ensuring they cannot be used to subvert or circumstep the mandatory access controls, and demonstating consistency with a top level specification. Cathy Jordan presented the last part of the paper, which described the DoDCSC policy on DAC. A set of guidelines is under preparation, which will discuss implementation and evaluation issues, and describe various mechanisms used to implement DAC (together with their benefits and drawbacks) for the benefit of evaluators and designers. The suggestiuon is that DACs are 'verified' by testing and penetration exercises, the aim being to check consistency with specification and conformance with Mandatory Access Controls. The guidelines will also cover those environmental control issues on which DAC depends, as well as various administrative issues. The first draft of the guidelines should become available in July, after consultation with major computer system vendors. #ABSTRACT#259# Protocols for use over V.24 (RS232); an addendum to the 'Yellow Book' service specification #ABSTRACT#260# A protocol is proposed to securely implement payment transactions between mutually distrustful parties. This protocol is designed to operate over an open network, and can be implemented using currently available encryption technology. #ABSTRACT#261# A probabilistic framework can be employed to assess the risk of disclosure of confidential information in statistical databases that use disclosure control mechanisms. We illustrate how the method may be used to assess the strengths and weaknesses of two existing disclosure control mechanisms - query set size restriction control and random sample query control mechanisms. Our results indicate that neither scheme provides adequate security. The framework is then further exploited to analyze an alternative scheme combining query set size restriction and random sample query control. We show that this combination results in a significant decrease in the risk of disclosure. #ABSTRACT#262# Previous title was Rex. #ABSTRACT#263# This booklet is a guide to how the 1984 Data Protection Act is expected to work in practice. #ABSTRACT#264# This report consists of an analysis of the field, sixteen invited papers covering important parts of the field in more detail, and an annotated bibliography of the papers and books referred to in the report. The analysis is a balanced report of the state of the art in management of secure computer systems. It does not deal with how to build a secure computer. Areas covered include the need for security, technical aspects (including physical security, hardware, software and communications, contingency planning and insurance), security management, security review and future requirements (including legal aspects). A good report, providing an excellent practical introduction to the subject. Ideal for someone who has some computers and wants to make the most secure use of them. #ABSTRACT#265# This paper aims to address the complicated issue of network security. Network security is approached in this paper from a functional and more specifically from a methodical point of view. A network can be seen as a collection of nodes that are connected by communication media in such a way that information can be transferred between nodes. The connection must be such, that resources like databases and printers may be shared between nodes. A node can be any computer hardware component and may even be another network like a local area network or a wide area network. Network security needs to be addressed from a technical as well as from an application systems perspective. The technological issues on network security addresses the broader concepts such as the provision of a variety of network security services and mechanisms for example authentication and traffic analyses. Applications network security assures that a network oriented application system be designed to adhere to the computer security policy of the organisation in general. #ABSTRACT#266# The IRR research model as proposed in this paper can be seen as an important first phase of a research process, aimed at formulating a new approach to risk analysis, risk assessment and risk management within the information technology environment. Over the past decade, considerable resources and efforts have gone into developing and automating risk analysis methods, in an attempt to make risk analysis more easily applicable and as a whole more successful. This resulted in a large number of automated techniques, methods and packages being currently available on the information security software market. The perspective the authors took in preparing this paper was to address the question "which approach combined with underlying business philosophies and business technologies?" This opposes the question usually asked by organisations, namely "which package?". #ABSTRACT#267# This a standard mathematical work presenting the theory of logic underlying, amongst others, the VDM and Z specification systems. #ABSTRACT#268# The Trusted X Window System (TX/WS) is a prototype of the X Window System for the TMach (trusted Mach) operating system. TX/WS is designed to support users manipulating information of different sensitivity labels simultaneously. In TX/WS, each top-level window on the screen may belong to a different application. These applications may be running at a variety of sensitivity levels. Each window is visibly labeled with the maximum sensitivity label of the application which created the window. To assist the user of a multi-level windowing system with overlapping windows, a visible labeling policy is required to avoid inadvertent misclassification of information. This paper describes a prototype which demonstrates various labeling policies for overlapping windows. It also summarizes feedback from the prototype. #ABSTRACT#269# This paper describes the early issues, obstacles, and ultimate achievements of Phase II of the DARPA Advanced Computing Systems project to develop a proof-of-concept prototype for a B3 X Window System on a TMach base. The paper defines initial project goals presents an overview of X, and describes system objectives. The major implications of meeting the B3 trust criteria and the constraints of building the Trusted X prototype on the TMach system (itself a prototype) are described. The paper leads the reader through the process of Trusted X evolution from an initial architecture requiring a large and complex TCB to an architecture based on task polyinstantiation greatly simplifying the TCB. #ABSTRACT#270# Multilevel secure windowing systems are a key technology for the 1990's. We have spent the past 20 months designing and implementing a prototype of a multilevel secure X Window System as a proof of concept vehicle for our software engineering process model for the development of trusted systems. The prototype is targeted to B3 evaluation criteria. In the early stages many doubted that B3 was achievable for a windowing system (especially X); we believe that our prototype demonstrates that B3 is achievable. This paper describes our goals, the architecture of our system, and some of the trade-offs we made to achieve our goals. It also contrasts our work with existing Compartmented Mode Workstations (CMW) windowing systems. #ABSTRACT#271# The MIT X Window System (X) has become a de-facto windowing system standard that is widely used throughout the computer industry. In many ways X is as important in the 1990's as standard operating systems were in the 1980's. Just as trusted versions of UNIX operating systems (from C2 systems such as Gould's UTX/32S to B2 systems such as AT&T System V Release 4/ES) are critical to bringing trusted systems into widespread use, trusted versions of X are necessary in order to make the full power of those trusted systems available to users operating in today's workstation environments. Adaptation of commercial systems to trusted systems generally involves tradeoffs between functionality and trust. X is no exception to this rule. Most commercial multi-user systems (such as UNIX and VMS) implement mechanisms that enforce various security policies, such as access control and privilege policies, although those mechanisms are often relatively primitive (eg. permission bits and super-user in UNIX). In contrast, X was explicitly designed to avoid enforcing any policies and, in fact, provides many mechanisms that tend to promote the sharing of data and resources among X applications. As a result, the tradeoffs between trust and functionality are far greater for X than typically encountered in operating systems. This paper surveys the issues and outlines various solutions to problems encountered in designing and building trusted X systems. The paper focuses on issues that appear both at the B1 and B3 levels of trust specified in the Trusted Computer System Evaluation Criteria, and in The Security Requirements for System High and Compartmented Mode Workstations. #ABSTRACT#272# This report consists of a sample policy and operating procedure for the handling of information within an organization. These form a good starting point for producing appropriate procedures for use within other organizations. #ABSTRACT#273# An Interorganization Network (ION) is a logical network imposed over one or more physical computer networks. The physical computer networks are owned by different organizations, and IONs are a way of supporting interorganization work. As well as supporting IONs, each physcial network supports a purely logical network. Estrin describes a way of maintaining separation between logical networks consisting of sets of facilities. In order to minimise the disruption of adding IONs to existing networks, two implementation constraints are identified: the implementation must not rely on physical separation, and those facilities that belong solely to an internal logical network do not implement any separation mechanisms. All messages entering a physical network enter via a gateway. The gateway only forwards the message if the source and the destination ION facilities belong to the same ION. ION facilities that belong to more than one logical network (IONs and the internal network) enforce separation between the different networks. Estrin's aim is to achieve a level of security equivalent to that achievable by other interorganization communication mechanisms such as phone and post. the final part of the paper identifies the vulnerabilities inherent in supporting IONs and how they can be removed so as to achieve this degree of security. This primarily concerns authentication issues. #ABSTRACT#274# This paper describes a protocol for enabling controlled use of the resources on the network for one organisation by systems attached to the network for another organisation. Each inter-net gateway acts as a border guard one behalf of its local network access control server (ACS), letting out only previously authorised traffic, letting in only previously authorised traffic, and redirecting authorisation requests to the ACS. Control of data flow within the network for an organisation is beyond the scope of this protocol. The protocol would appear to do the job for which it was designed, though it is not optimal - too many messages are rejected by gateways (returning the address of the local ACS) instead of being directly forwarded to the local ACS. #ABSTRACT#275# Note: This paper describes some of the security related problems that may be encountered when communication is required between/via separately owned, maintained and run networks (Autonomous Regions). Policy Routing is a technique that is used to choose an appropriate route through several autonomous regions based on policy related parameters such as cost and access rights. The paper explains the potential threats that can be posed to policy routing protocols (i.e. falsification of policy routes, misuse of valid policy routes and denial of service). It then goes on to describe and analyse mechanisms designed to prevent these sorts of attack. The main technique described by the paper is the use of encryption of the communications between the policy servers of the interconnected autonomous regions (the entities that generate and distribute policy information throughout the networks). The encryption of relevant information is used to ensure that the information being passed has been generated by an authentic policy server and that it has not been modified in any way. A general scheme for a secure policy routing protocol is presented which details the steps that any variation of protocol should take. The steps include a secure mechanism for distributing session keys to all of the autonomous regions in the selected route and ways in which senders of packets of information from one autonomous region can be authenticated by entities in another. The final part of the paper examines the costs incurred in using a scheme such as the one described and concludes that for a sample (3 hop) policy route using DES encryption, the costs incurred range between 9% and 28% which is a rather high figure. #ABSTRACT#276# In this paper we describe a visa scheme for implementing access control in Inter-Organization Network (ION) gateways. The purpose of the scheme is to allow an organization to modify and trust only those internal systems that require ION access; all other internal systems can not communicate with the outside. Control is distributed among the ION participants so that each may make its own design tradeoffs between performance and trust. It is desirable to implement controls at the network, i.e. packet, level because of the relative performance, flexibility and ubiquity of network-level gateways. However, a new mechanism was called for because the only information available to existing network-level gateways is the network-level address in the packet header and such network-level addresses do not carry the higher-level, logical information (e.g., organization affiliation) needed to make access control decisions. To overcome these problems, a visa ION gateway woeks in concert with an Access Control Server (ACS). The ACS carries out high-level evaluation of communication requests and the gateway enforces the ACS's decision using the visa scheme. In order for a node to send a packet through a visa gateway, the node must obtain a key(visa) from the ACS of the visa-controlled networks that it wishes to leave and enter. If the node passes an ACS's policy filter, the ACS gives its local gateway the source and destination nodes' network IDs and a visa with which to authenicate packets coming from or to the source node as they pass through the gateway. The same visa is given to the source node to stamp all outgoing packets for the duration of the session. To prevent or inhibit the acquisition of visas through interception of packets, the stamp included in each packet is a function of the visa and the packet checksum. #ABSTRACT#277# This paper discusses some of the issues in meeting the Compartmented Mode Workstation (CMW) requirements while still supporting commercial applications. The reader is assumed to have a general familiarity with CMW and window systems. The security policy is summarised, and followed by a discussion of how it has been interpreted in the real world of X11 programming. Applying restrictions to the X protocol prevents clients from interfacing with each other, while still providing enough functionality to make these programs useful. Special considerations are given to the root window, selections, grabs, and atoms to meet the needs of existing applications. #ABSTRACT#278# Considerable experience has been gained in Government funded or controlled facilities in the United States, in the UK and elsewhere in the evaluation of systems and products. This paper discusses experiences gained from the operation and management of a UK Commercial Licensed Evaluation Facility (CLEF), and highlights the issues involved in the marketing of certification to security product vendors. #ABSTRACT#279# The states of knowledge that are attainable in distributed systems are characterized, where communication is done by unreliable message exchange. The reason that certain states of knowledge are unattainable is a conservation principle which says that information about 'nature' that can be obtained by combining all of the knowledge of the members of a closed system is preserved. The class of formulae in the propositional modal logic of knowledge are axiomatised, and the complexity of the decision problem is determined. #ABSTRACT#280# The Distributed Computing System is an information utility designed to provide reliable, fail-soft service at relatively low cost to a large class of users with modest requirements. The salient feature of this system is the distribution of hardware, software, and system control. Hardware distribution is achieved using a local area network architecture. Software and control distribution is facilitated through the use of communication by name, rather than address, among the network components. The combined effect of distribution, which provides both redundancy and isolation, and of controlled access, makes total failure of the computing system unlikely. Reliability is achieved by minimizing the probability of total failure, using isolation to keep local failures from spreading and causing global failure, and using redundancy to negate the effects of local failures. This paper is quite brief, although it includes a number of references to more detailed earlier papers. It describes the organization of the DCS hardware system (a digital communication ring) and the resident system services in each processor on the ring. Processes are distributed about the ring and their relative positions are invisible to each other. The functions needed to protect the system and to provide resource allocation are dealt with: resource allocation uses a broadcast system in which resource allocator processes bid to provide requested resources #ABSTRACT#281# This paper proposes a three stage method for obtaining a verified design. It gives step-wise guidance in the application of the verification process at various stages. The guidelines are derived from experience gained in the verification of a particular processor, the Restricted Access Processor, RAP. Appears to be worthwhile reading. #ABSTRACT#282# A relatively weighty tome about the SRI/MLS model, SPECIAL and the Boyer-Moore theorem prover. Probably of interest only to those who are getting involved with these specific topics. #ABSTRACT#283# This is a long and fairly dense paper. It is mainly a review of issues. The main conclusion is the need for another category C2-a between C2 and B1 to be used by industry until B1 products become available. The attributes of C2-a are discussed informally. #ABSTRACT#284# Note: The authors are interested in developing a security model for an object-oriented database. This work is necessary as previous database security models only apply to relational databases and these are not rich enough to cope with object-oriented databases. The work done is in the context of the database OSAM* which is being developed at the University of Florida. However, the authors believe that the work can be generalised. Before defining the model, a number of issues are considered. Should the database be open (only preventing access which is forbidden), which is good for flexibility, or closed (only allowing access which is permitted, which is good for security? Should the database have positive or negative authorisations? Should the database uphold a MAC or a DAC policy? Only the last of these questions was really answered. The authors chose a DAC policy. The security model has three components; policies, a structure of authorisation rules, and an algorithm to evaluate access requests against the authorisation rules. The policies are independent of security requirements and define access to the database. These policies are: „ A user who has access to a class can gain similar access to all the inherited attributes of its subclasses; „ Access to a class implies access to all the attributes of that class (including inherited attributes); and, „ It is not possible to access the non-inherited attributes of a class by accessing a super-class. The authorisation rules consist of a set of triples; users, accesses, and object attributes and say which users have what accesses to what attributes of what classes. There are also administration rights which dictate who can change the authorisation rules. However, nothing is more is said about these. The notion of a security context is then introduced. A security context is a subset of classes in which a query can be answered. The set of classes of a security context form a partial order in terms of class associations (ie, subclass and superclass). To answer a query within a security context, the authors define a Security Query Graph (a subset of the security context) and an algorithm for searching this graph. Finally, the authors suggest possible extensions which are more efficient. #ABSTRACT#285# Computer systems take on security requirements that are unique to the operational characteristics and needs of their application. These requirements can be applied on an individual basis in reducing operational risk. Methods exist to determine security requirements per DoD 5200.28-STD by calculation of a risk index. This risk index is used to determine an appropriate level of trust (criteria class) per DoD 5200.28-STD, which is then used to define a set of security requirements. However, the resulting security requirements imposed on some systems by DoD 5200.28-STD can be overly restrictive, in need of interpretation, or in many cases non-applicable. The purpose of this paper is to provide insights into determining appropriate security requirements for applications within a specified criteria class. Observations depend to a great extent on the system's user interface, considered as an additional environmental condition. Computer systems take on security requirements that are unique to the operational characteristics and needs of their application. These requirements can be applied on an individual basis in reducing operational risk. Methods exist to determine security requirements per DoD 5200.28-STD by calculation of a risk index. This risk index is used to determine an appropriate level of trust (criteria class) per DoD 5200.28-STD, which is then used to define a set of security requirements. However, the resulting security requirements imposed on some systems by DoD 5200.28-STD can be overly restrictive, in need of interpretation, or in many cases non-applicable. The purpose of this paper is to provide insights into determining appropriate security requirements for applications within a specified criteria class. Observations depend to a great extent on the system's user interface, considered as an additional environmental condition. #ABSTRACT#286# Acquisition interface, written in the ELLA Language, is presented together with simulation results. Comments on the present Control acquisition scheme of the current D7.3 version of the Futurebus specification are also included. #ABSTRACT#287# This memo offers guidelines to programming the STAB II microengine using the STAMP language. It has been written to show how the configuration of the hardware influences the microprogram and details any restrictions on the STAMP microprogram. #ABSTRACT#288# This memo describes the Instruction Fetch Unit for the SMITE Workstation. It is an autonomous device fetching instructions from the local store and providing a degree of preprocessing from the microengine. #ABSTRACT#289# This memo discusses the various numerical algorithms used by the STAB II secure workstation together with a brief treatment of the theory of the various operations where appropriate. #ABSTRACT#290# This memo describes the microprogram interface to the STAB II Video Card. This includes accessing the Graphics Processor and associated palette drivers, the keyboard and the mouse interface. #ABSTRACT#291# This memo is a description of the STAB II Secure Processor for SMITE main CPU hardware together with the software implications of that hardware. #ABSTRACT#292# This memo describes how to use the Cudgel language to describe the hardware connectivity and control structure of the STAB Il computer. The cudgel description is used by the SMITE micro-assember development system (SMAC) to produce loadable microcode from the STAMP microprogram. #ABSTRACT#292# This memo describes the use of a Texas TMS34061 Video System Controller with the current lMbit VRAMs. The STAB II Secure Workstation Video Card is used as an example. It is shown that the requirements and functionality of a secure workstation need not be compromised by the use of a simple interface to the screen buffer. #ABSTRACT#293# This memo describes the microprogram and Algol68 interface to the STAB II Video Card. This includes accessing the Graphics Processor and associated palette drivers, the keyboard and the mouse interface. #ABSTRACT#294# The SMITE computer architecture is being produced as a base for computer security applications. This paper describes the instruction set level of SMITE, which is based upon the Flex capability computer architecture. #ABSTRACT#295# This memo describes the literate programming approach to ELLA Using Donald Knuth's WEB System. The system enables the ELLA program and its documentation to be bound together in one file. The memo, apart from this title page and the Appendices, was produced directly from a WEB file. This WEB file W.IS also used to produce the program which was run on the ELLA system. #ABSTRACT#296# This memo describes the software interface between the Perq microcode development systems and the STAB II Secure Processor. It also details the interface for the systems real time clock. #ABSTRACT#297# This article formed the basis of report IS50-550, Datapro Reports on Information Security. #ABSTRACT#298# This report was based on an article of the same title in BYTE volume 11 issue 4 (1986) #ABSTRACT#299# Note: This paper is useful from a methodological point of view. It is about a method for analysing systems for satisfaction of Noninterference properties. Thus it is not concerned with theoretical analysis of information-flow models as such, but rather with what it takes to apply a given one, Noninterference, to perform a security analysis of a given system. The author is from the Honeywell-owned Secure Computing Technology Corp. It is not quite clear what is the starting point of analysis. For example, the analyst must have a very thorough knowledge of the system and yet the relevant state-variants are to be discovered by the analysis, not available from a specification. The starting-point appears to be a low-level implementation-specification, such as might be written in Gypsy. The main point of this method is the need, characteristic of noninterference, for a definition of when two states are equivalent with respect to a given security-level. The author says there is no strong rationale available for constructing this relation on states, and so an algorithm is given. The algorithm is to make initial guesses for the set of assumptions which constitute a state-invariant and the equivalence relation. The guess is repeatedly improved, at each step introducing for consideration another one of the systems operations. The example given was for a system which is a security-kernel, and the operations are kernel-requests. For each operation, the current guess for invariants and equivalence relation is modified until three conditions are satisfied for the operation. These are: state-invariants preserved, old-state and new- state equivalent at appropriate security-level, and equivalent old- states produce equivalent new-states. These conditions amount to an unwound form of the non-interference property. Inability to prove the first of these means the list of assumptions of the state invariant must be extended. Inability to prove the second means either there is a covert channel or the state is unreachable or the equivalence relation is too strong (has identified some high- level part of the state as visible at low level). Inability to prove the third means the equivalence relation is too strong or too weak (does not identify all portions of state visible at low level). An advantage is said to be that failure at any step does not invalidate the analysis work done in previous steps. Mentioned in the presentation, but not in the published paper, was that by keeping track of reason for each extension, an attack scenario may be constructed; no details given. The method has not been applied to a real development. A method is described for constructing an appropriate equivalence relation for a noninterfereence analysis. This method is constructiv in the sense that it can bwe applied as the system is developed instead of at the end of the design process. Additionally, the method addresses the question of the correctness of the equivalence relation. #ABSTRACT#300# Note: The Distributed Trusted Mach (DTMach) program is developing a design for a high-assurance, secure, distributed system based on Mach. To achieve this goal, it is first necessary to identify the general threats against which DTMach must protect. The next step is to identify control mechanisms that are sufficient to protect against each of the threats. The DTMach design makes extensive use of type enforcement in ad- dressing the threats. This paper describes the general threats and the countermeasures provided by DTMach. Doing so provides more evidence of the usefulness of type enforcement in general and the high assurance provided by the DTMach type enforcement policy. #ABSTRACT#301# This paper presents a new approach, based on finding shortest paths in a graph, for solving the cascade problem. The result is an efficient (O(N^3)) algorithm, where N is the number of security domains in the network. The paper provides background on the cascade problem, generalises the problem from its traditional military roots, and then applies the shortest path technique to a military example. The shortest path approach appears quite general and provides a method based on established mathematics for evaluating network security. #ABSTRACT#302# Note: This paper describes the way in which smart cards and biometric devices can be used to enhance user authentication procedures. It also looks briefly at encryption. #ABSTRACT#303# This report lays the foundation for a new model and approach for secure information flow. The model is driven by lattice based information flow policy, which describes the permitted dissemination of information in the system. System entities are allowed to handle different classes of information from the flow policy, and information is permitted to flow between entities so long as they do not violate the flow policy.With this conceptually simple notion of security we can describe many interesting security properties, for example traditional multi-level policies, aggregation policies, and chinese walls. Details are given on how secure systems based on the model can be implemented in practice. We also examine how other types of security policies, such as integrity and separation of duty, can be defined in terms of lattice based policies. #ABSTRACT#304# This report proposes a structure for describing information flow policies that can express transitive, aggregation and separation (of duty) exceptions. Operators for comparing, composing and abstracting flow policies are described. These allow complex policies to be built from simpler policies. Many existing confidentiality (and by using a dual model, integrity) policies can be captured in this framework. A high water mark model is developed that can enforce these information flow policies. This model provides the basis for a taxonomy of existing high water mark mechanisms. #ABSTRACT#305# Note: The author presented a model that can describe non-transitive information flows. The trick basically is to associate with an entity A in the system two classifications AH, AL drawn from a lattice, with AL ð AH. We then require that: „ information in A can flow to any class a only if AL ð a; and, „ information at any class a can flow into A only if a ð AH. The idea is developed in a number of rather theoretical, ways. For example, the author shows that one can define an algebra of such models. This is reminiscent of MacLeanðs presentation the previous year. The idea is neat but more thought is needed to assess its practical utility, in particular as contrasted to, say, assigning caveats in the time honoured fashion or indeed the assigning of both integrity and secrecy labels to entities. The author remarks that the model may be suitable to describe part of the Clarke-Wilson model. A neat piece of work that merits closer attention to evaluate its practical utility. #ABSTRACT#306# This paper proposes a notation for describing information flow policies that can express transitive, aggregation and separation (of duty) exceptions. Operators for comparing, composing and abstracting flow policies are described. These allow complex policies to be built from simpler policies. Many existing confidentiality (and by using a dual model, integrity) policies and their models can be captured in this framework. A high water mark model is described that can enforce a large class of these information flow policies. The model provides the basis for a taxonomy of existing high water mark mechanisms. #ABSTRACT#307# Note: Modelling both the system and its users as concurrent sequential processes and using a theory recursively based on CSP primitives, this paper formally describes the relation between a system and a user who meets the interface implied by the system's behaviour specification. Such users never engage in events that the system finds unexpected. Information can flow from one such user to another if it can engage in a trace (with the system) which will ensure that another user is prevented from engaging in one of its own. This definition is thus similar to that for deducibility. This property of a system, between the two users, is called dependency and can be proved or disproved using CSP. Dependency is generalized to a property (leakage) which includes the possibility that some additional environmental process (eg a third user or group of users), when working in parallel with the system, will then produce a dependency between two users - although the paper does not describe how these environmental processes are to be found. #ABSTRACT#308# This paper gives an outline of the history of SCOMP and an overview of its likely application areas. It goes on to describe the updated processor succeeding SCOMP, the DPS6 plus, and its operating system STOP 3.0. The new single processor has 70% better performance, and can be expanded up to a 4 processor system. #ABSTRACT#309# This paper is an introduction to the SCOMP software and hardware architecture. It includes a short section describing the SCOMP security kernel. #ABSTRACT#310# This paper presented a technique to protect files on distributed systems from being usefully accessed by an intruder while simultaneously providing a degree of fault tolerance. The method is to split up an encrypted file into a number of fragments, which are stored on different archive machines (each fragment on more than one, but not all on one machine). If an intruder gains access to an archive machine, some of the fragments may be compromised, but use of a stream cypher means that a copy of each of the fragments are needed to read all of the file even if the cryptographic key is compromised. No application (as yet), as the project is just starting. #ABSTRACT#311# The paper shows how Security Information for user authentication, peer-entity authentication and access control is created and utilised in large distributed systems. The protection mechanisms used are hash functions, symmetric and asymmetric cryptography. We describe and combine data formats for Security Information based on international standards from several standardisation bodies. #ABSTRACT#312# During the past three years, we have investigated how to certify the trustworthiness of application systems built to satisfy stringent security requirements and have undertaken the certification analysis of two command and control systems targeted at the B3 class of the DoD Trusted Computer System Evaluation Criteria (TCSEC). Based on these experiences, we have gained many insights into the certification and procurement of trusted application systems. Certifying a trusted application system in a contractual environment presents both technical and programmatic challenges. The procurement policy must to some extent take into account the certification approach. This paper documents some of the lessons learned during our investigations. #ABSTRACT#313# Only for people with a strong mathematical background. #ABSTRACT#314# This paper describes changes made to a network protocol in order to make it "trusted" in a multi-level secure operating system. The protocols are the standards used by the Internet; the Transmission Control Protocol and the Internet Protocol (TCP/IP). These protocols are currently used in many heterogeneous networking environments. This paper is based on actual work being done by AT&T Bell Laboratories and The Wollongong Group in the joint design and development of a secure TCP/IP. #ABSTRACT#315# This paper sets out to consider the implications of the use of 'smart' terminals and workstations with mainframes. However it does not seem to come to any particularly striking conclusions as to how they should be treated to ensure security. #ABSTRACT#316# An interesting paper on the problems of designing autonomous robots, where the primary aim is prevention of denial of service, and the security needs include physical protection, operational integrity, secrecy of intentions, capabilities and knowledge. A major problem is that of false information or orders via its sensors or communications links. The paper categorises the generic threat types and attempts to stimulate interest in a field not directly related to the problems of multilevel security. #ABSTRACT#317# The Joint MLS Technology Insertion Program was established by the Joint Staff J6 in January 1990. A key component of the Joint MLS Program is the DoD testbed at Military Airlift Command (MAC), Scott Air Force Base (AFB), Illinois. The testbed is addressing critical secure system integration issues associated with expediting the deployment of MLS capabilities and components into operational command and control systems. This paper will discuss the activities, successes, and challenges associated with the testbed activities at MAC. #ABSTRACT#318# Note: This paper discusses the problem of fitting 'trust' to off-the- shelf applications (conversion), as well as that of producing new trusted applications (development). #ABSTRACT#319# Note: This speaker argued that not even compilers may be trusted to generate virus-free code, since it would be quite possible to infect a compiler in such a way as to infect all code which it compiled. From this he argued that the only way to be sure that compiled code is virus- free is to disassemble it and compare it with the source code. He further argues that all viruses must contain a conditional statement to perform their triggering action, and that only these need to be disassembled to achieve the objective. This paper was not generally well-received and attracted an amount of criticism. The speaker appears to ignore the strong possibility that it would be easier to write and fully validate a compiler rather than write a suitable disassembler. The technique would not be applicable to an optimising compiler, since the expressions found in the executable code would not necessarily resemble those in the source code. It is also not clear that a virus must contain a conditional statement, and it would seem that the use of boolean computations and jump statements could be used to achieve the same effect whilst bypassing this detection method. #ABSTRACT#320# The advent of decentralized computing and an increasingly important role for information as a resource has prompted the development of a variety of methods and tools for managing the risk exposure of a computer system. As a result of the diversity of risk management tools currently available, there is no effective means of determining which of the tools would be most suitable for any given organization's situation. A new technique is proposed to effectively and objectively evaluate these tools for suitability and to establish a means of comparison of the tools among each other. #ABSTRACT#321# Note: This is the second of three papers at the symposium on secure databases from TRW. ASD stands for A1 Secure DBMS or possibly Advanced Secure DBMS. In order to be reasonably self-contained about half of this paper presents material familiar from the Wilson paper (above). It continues the exposition of database views as classified objects. I'm not sure two separate papers are justified, and will give this one only a short report. The main theme is the importance attached to getting the TCB down to a 'small' size, or relatively small, necessary for certification at B2 or better. The problem is that in general, view-processing is a large part of all the code of the DBMS. What is needed here is a trusted view-processor. The method of getting a small trusted view processor is to restrict the query-language used for defining of views for security. A secure view is allowed to be defined only in terms of a single base relation (ie no joining of relations necessary). The amount of trusted code in the view processor is then only 1000 lines, in addition to the DBMS's trusted record-level interface. No other numbers are given for comparison. This paper describes a proposed approach rather than a working system. ASD_Views is an implementation of views as the security object in a multilevel secure relational Database Management System (DBMS) that results in a small trusted computing base (TCB) as required to meet the criteria for evaluation class B2 and above. A general view is the result of a database query. Since most of the code which implements the DBMS is involved in processing the query, most of the DBMS must be trusted. ASD_Views are defined using a subset of the relational algebra to restrict the size of the query language available to define a secure view. This approach reduces that part of the TCB required to implement secure views to roughly 1,000 lines of code. Although ASD_Views restricts the functionality available in the view definition, the flexibility is still greater than if the row or column is the security object. In addition, views preserve data integrity by using the contents of the data as the basis for its sensitivity label. #ABSTRACT#322# This paper introduces model-based reasoning and discusses how model- based reasoning capabilities can be applied to intrusion detection. We discuss the benefits of the approach and have shown its advantages over those currently in use. The use of model-based reasoning technology allows intrusion models to be specified much more easily and naturally than is the case using other techniques. Most importantly, the use of model-based reasoning technology will allow IDES to be a much better detector of intrusions. #ABSTRACT#323# Note: Also published by SRI. We discuss work aimed at defining a multilevel, mandatory security policy for knowledge based systems. We address two distinct issues: an effective implementation formalism based on a multilevel, object- oriented programming paradigm, and requirements for ensuring the correctness of inferences computed on the basis of possibly contradictory information from different access classes. We define requirements for an object-oriented system capable of handling multilevel objects within a single access class. We then outline a method by which multilevel objects may be used to implement a simple knowledge based system built on production rules. We argue that the issues regarding correctness are similar to those of truth maintenance in standard knowledge based systems and may be addressed by similar methods. #ABSTRACT#324# Note: This book documents well the US philosophy on security including their emphasis on practical progress and scepticism of novelty. Attitudes seem to include: Models - state based, non interference still theoretical. Integrity - mostly academic interest. Capabilities - new-fangled machines with little practical use. Particularly relevant are chapters: 5 - Principles of a Security Architecture 9 - Security Models 11 - Architectural Considerations 12 - Formal specification and verification. #ABSTRACT#325# Note: Distributed at 4th Aerospace Computer Security Applications Conference as Tutorial Notes. #ABSTRACT#326# Note: This paper discusses an architecture for the delegation of privilege within a distributed system. The method described is intended to form part of Digitalðs Distributed Secure System Architecture (DSSA). The idea underlying the approach is that public key cryptology can be used to provide authentication without the need for an authentication server. The paper uses Girling [PhD Thesis 1983] as an example of the authentication server approach. Typically a user will wish to access resources on some remote device (e.g. a server) through a series of nodes (e.g. workstation). This process involves delegation of privilege from the user to the first workstation, from the first workstation to the second workstation, et. seq. At each stage of the process a certification is generated which is signed by the delegating node and states that the delegated node may act on its behalf. The server collects together all the certificates and is able to reconstruct the chain and so deduce the identity of the originator of the request. The certificates are public. However signatures may only be verified by the generating node. This is achieved by a public key scheme in which each node generates a private key/public key pair. The public key is entered into the data portion of the certificate while the private key is used to generate signatures. The private key is never released from the generating node. When a user terminates a session he is able to request of all nodes in the chain that they delete their private keys. This means that the certificates become useless since they cannot be verified. Hence the system protects the user against a node being subverted after he has terminated his session. It does not, of course, provide protection against a node which is subverted during the session. The paper goes on to discuss refinements to the level of privilege that is delegated and also to discuss performance. It is pointed out that signature verification will be much more frequent than digital signing and suggestions are made to exploit this. Key generation is acknowledged to be a problem, especially since the architecture requires a new key for each delegation in each chain. The authors suggest several enhancements in this area and conclude by putting a wet finger in the air and claiming that some of the enhancements must surely be good enough. Delegation is the process whereby a user in a distributed environment authorizes a system to access remote resources on his behalf. In today's distributed systems where all the resources required to carry out an operation are rarely local to the system to which the user is logged in, delegation is more often the rule than the exception. Yet, even with the use of state-of-the-art authentication techniques, delegation is typically implicit and transparent to the remote system controlling the resources, making it difficult for that system to determine whether delegation was authorized by the user. This paper describes a practical technique for delegation that provides both cryptographic assurance that a delegation was authorized and authentication of the delegated systems, thereby allowing reliable access control as well as precise auditing of the systems involved in every access. It goes further than other aproaches for delegation in that it also provides termination of a delegation on demand (as when the user logs out) with the assurance that the delegated systems, if subsequently compromised, cannot continue to act on the user's behalf. Delegation and revocation are provided by a simple mechanism that does not rely on online trusted servers. #ABSTRACT#327# This gives a design for a LAN that uses TIUs for separation. The TIU for an untrusted node will label all messages with the classification level of the node, and will only accept messages with the appropriate classification level. The TIU for a multilevel node will accept all incoming messages in a range of security levels, and will check that the security labels of outgoing messages lie in the same range. The design makes no attempt to provide authentication; the LAN is assumed to be physically secure and TEMPEST-proof. #ABSTRACT#328# Note: Report No T/4060T3/3100/17. #ABSTRACT#329# This compact and up to date volume introduces the reader to the low level details (OSI's physical and data link layers) of an impressive array of local area networks. After first placing local area networks into their historical context it gives separate chapters to the topologies that can be used, basic data transmission techniques, and major requirements in terms of hardware and software. A chapter on example local area networks that have been implemented and extensively tested includes Ethernet, Cambridge Ring and broadband systems. It covers a number of commercially available networks explicitly. After a chapter giving a non-mathematical consideration of performance characteristics the book is concluded with a brief list of possible local area network applications. There is a small number of relevent references at the end of each chapter #ABSTRACT#330# This paper presents a mechanism for sealing an object using a key. It gives details and mathematical proof of the sealing mechanism, and also considers the systems aspects of the way in which sealed objects can be used to solve various problems in distributed computing. #ABSTRACT#331# This paper presents an investigation into a typical local area network's susceptibility to covert channels in the use of its low level protocols (which will often be available even in secure network architectures). Both storage channels and timing channels are identified. Results of a simple experiment on the BBC micro's Econet are then given which are demonstrative of the large bandwidth that can be associated with a covert channel based on address data. Some possible bandwidth reduction techniques are discussed, including their cost and (in)effectiveness. #ABSTRACT#332# This report gives a detailed design of an object authentication scheme for use in a distributed system, and its implementation as part of the Cambridge Distributed System. Chapter 5 (pp. 32-42) provides a good overview of the work done in the area of authentication of objects on a network. #ABSTRACT#333# Note: Also appears in IEEE Software Engineering Notes, Vol 10 (4), pp76-79. #ABSTRACT#334# Note: Operator nets are represented by an interconnected set of nodes each arc of which represents a sequence of messages. The nodes themselves represent processes, may have several input arcs but only one output arc, and are associated with a particular processing function. Using this simple model of a distributed computing system this paper describes a history (a set of incomplete message sequences from each of the arcs in the net), an event (two histories and the set of executing processes that take one to the other), what it means for an event to cause a message, when one event can be said to precede another (without recourse to the physical notion of time), and what one message depending-on another means. Knowledge is taken to be a set of formulae derived from iterative reasoning about an initial set of axioms in conjunction with knowledge explicit in each message the process has ever received. The above notions are then used to build up corresponding definitions involving knowledge including: an event Kcausing a process to know a formula (i.e. a fact); the knowledge of one formula by a process Kpreceding the knowledge of another formula by another process; and the knowledge of a formula by a process Kdepending-on another process. A number of security properties are then defined using these knowledge orientated relationships. The first two security properties (knowledge noninterference security and knowledge independence security) express non-interference for non-deterministic systems and are informally proven to be equivalent and composable. The proof of composability assumes that the interfacing processes which are used to generate outputs to one system and receive inputs from the other are non-reasoning and have the same security levels. The third security property definition, for knowledge security, requires knowledge to have a related security level and simply states that a process may only know a formula with a classification that the process dominates. This is a very simple and high level description of security which, unfortunately, would prove difficult to verify against in practice. The final two properties were not presented but are in the paper. The knowledge integrity security property is just the dual of knowledge noninterference security using integrity levels. It prevents processes with high integrity classification knowing formulae through the activity of lower processes. Finally, authority systems security is equivalent to knowledge noninterference security except that it relaxes the noninterference requirement for highly classified processes which possess a particular axiom in their initial set. It allows such processes to determine the level of the formulae they deduce themselves (and would, therefore, accommodate systems in which a process can perform reasoned downgrading). The implementation of operator nets in 'LUCID' and the unfinished construction of a proof system for the security properties are also mentioned. Much of this paper, and in particular the knowledge security property, is relevant to the UK work on the theory of security. A method for reasoning about knowledge in multilevel secure distributed systems is introduced. This method, based on a behavioural semantics for operator nets, can be used to specify a variety of security properties, such as nondisclosure, integrity, and authority systems. The major attributes of the method are the intuitive nature of the specifications, and the expressibility of the model which allows statements about temporal properties and deductive capabilities of processes. #ABSTRACT#335# The presentation differed from the paper in the proceedings, which was a review of what Honeywell did in the light of guidelines subsequently produced for the DoDCSC and of comments on an earlier paper (April 1983). #ABSTRACT#336# The purpose of this document is to define a set of guidelines for Trusted Facility Management and Audit in secure computer systems. These guidelines elaborate the requirements of the reference [TCSEC 83] in these two areas, and define the functions, databases, and mechanisms of the system administrators (ie the security administrator, the trusted system programmer and the account administrator), system operators (ie secure operator, operator) and the auditor. However, the assignment of trusted facility management and audit roles to specific individuals is not addressed herein; such assignments must be left to the management of specific installations. The relationships between the guidelines and the requirements of the reference [TCSEC 83] are presented both in the area of trusted facility management and in that of audit. Although the guidelines are abstract (eg, they are unrelated to the mechanisms of any specific system), they are sufficiently detailed to serve as an architecture-definition document in both areas. #ABSTRACT#337# This paper describes an implementation by IBM of a secure version of a UNIX look-alike on a personal workstation. The aims were threefold: to provide a compatible interface to UNIX V; to achieve multilevel security somewhere between B2 and A1 on the NCSC scale; and, to have minimal, incremental performance penalties. Despite the problems of difficulty of verification and testing, and of having two coexistent security policies, it was decided to enhance an existing implementation to provide security rather than provide an emulator on top of a separate security kernel. The paper describes in detail the Access Control List mechanism that was added to provide finer granularity of discretionary access control, and then describes the lattice-oriented mandatory access control mechanisms. These mandatory controls assign a current clearance to each process, based on the runtime clearance of the user (dominated by the maximum for the user and the group) and of maximum clearance of the user's terminal; note that the user must have been able to set up a clearance higher than a minimum value associated with the terminal. As well as groups and users having security profiles, so do workstations, reflecting the profiles of attached terminals and attached private devices. After describing the way the mandatory controls are integrated into the system, the paper discusses the accountability policies and mechanisms, including user identification, the secure attention key, auditing, and the system management functions. An appendix describes the then current security levels, consisting of a heirarchical component of up to 256 elements, and a category set of up to 40 independent elements, and then describes the ordering relation that makes these levels a lattice. #ABSTRACT#338# When developing secure systems, there should be a testing process in addition to any formal verification procedure. This paper presents a way of reducing the number of tests in a systematic fashion by eliminating redundancy; the method has been used to assist in the testing of a secure version of UNIX. The ideas underlying the paper appeared to be sensible and useful, but unfortunately were very badly presented. Note: automated testing adds a level of indirection; how sure are you that the test tools are correct? #ABSTRACT#339# In this paper we define and rationalize a policy for propagation of authentication trust across realm boundaries. This policy helps limit global security exposures that ensue whenever an authentication service is compromised. It is based on a hierarchical model of inter- realm authentication, and can be supported by both public-key and secret-key systems. As an example, we present a simple protocol which selects inter-realm authentication paths of a design which provides application transparency for inter-realm, authentication-path selection and acceptance as the default mode of operation. The design can be integrated with the security services of existing systems; e.g., of the Open Software Foundation's Distributed Computing Environment (DCE). DCE implementation issues are also discussed. #ABSTRACT#340# This paper describes what happened when people attempted to retrofit security to VM/370. It is very readable, it explains just how hard it is to patch on a security model to a large system that is being independently developed. There is a good deal of sound advice summarised at the end of the paper. #ABSTRACT#341# SIFT (Software Implemented Fault Tolerance) is an experimental fault- tolerant computer system for flight control of advanced aircraft including those that are inherently unstable. Such a computer must be extremely reliable. Life-testing and exhaustive testing of such a computer are both impossible. To justify their claims of high reliability the designers of SIFT have had to verify that the design is consistent with the required fault-tolerant behaviour. This paper first outlines the basic fault-tolerance approach, the design philosophy, the hardware and software structures used. It then describes the way in which the design was verified #ABSTRACT#342# The paper described ICAP, an Identity-based CAPability system. ICAP is aimed at a distributed network environment in which certain problems arise when a traditional capability system is used. For instance, it may be necessary to pass a capability for an object to a user via an intermediary. Using a traditional system, this would also enable the intermediary to gain access to the object. The solution taken by ICAP is to check against the security policy whenever a capability is propagated. This ensures that only authorised users gain copies of any capability whilst minimising the performance impact. The problem of ensuring that only the trusted server is able to propagate capabilities is solved by including the recipientðs identity in each capability so that it can only be used by the intended user. When a capability held by a user for an object is to be revoked, an exception list for the object is updated making useless all copies of the capability for the object held by the user. By keeping track of the propagation history for a capability, the OS can ensure that only the relevant users can revoke the capability. #ABSTRACT#343# Note: The authors claim that suprisingly many protocols donðt work - despite the fact that they are small. They will often contain flaws and vulnerabilities that escaped detection as it is difficult to consider all attacks and the security claims are not presented in a systematic way. The object of the paper is to improve on the earlier BAN logic so that protocols can be specified and analysed in a systematic fashion. The basic notions of the approach are of principals (state machines), protocols (distributed algorithms), messages (the means of communication between principals), formulae (bit strings), and sets of beliefs and possessions (formulae) known to each principal. It introduces the concept of ðfreshnessð (a message is not a replay of a message prior to this session) and recognizability (the recipients expectations of the message are satisfied). A notation for expressing the reasoning process is presented (informally in the body of the paper, and more precisely in an appendix), together with rules representing the logical postulates of the reasoning process. The methodology is used to analyse the Needham-Schroeder algorithm; as one would hope, the known flaw was revealed together with another, minor one. Further work is required, to get the current design to a stable state, and then to extend it to support additional properties for the protocols. However, to handle aspects of information leakage, more significant changes may be required. The methodology, once extended, needs to be further tested by analysing other protocols. In the questions that followed the presentation, Dan Nesset claimed that whereas, like BAN, the new methodology can show flaws, it cannot say if a protocol ðworksð as it can only cope with known types of attack. Analysis methods for cryptographic protocols have often focused on information leakage rather than on seeing whether a protocol meets its goals. Many protocols, however, fall far short of meeting their goals, sometimes for quite subtle reasons. We introduce a mechanism for reasoning about belief as a systematic way to understand the working of cryptographic protocols. Our mechanism captures more features of such protocols than that given in a recent work [1], to which our proposals are a substantial extension. #ABSTRACT#344# A new key distribution scheme is presented. it is based on the distinctive idea that lets each node have a set of keys of which it shares a distinct subset with every other node. This has the advantage that the numbers of keys that must be distributed and maintained are reduced by a square root factor; moreover, two nodes can start conversation with virtually no delay. Two versions of the scheme are given. Their performance and security analysis shows it is a practical solution to some key distribution problems. #ABSTRACT#345# Note: Also published as Stanford University SEL Technical Report 86- 292, January 1986. #ABSTRACT#346# This is the standard reference describing GVE, the Gypsy Verification Environment, by the person who headed the team that produced Gypsy at the University of Texas at Austin. #ABSTRACT#347# This useful review starts with a amusing historical introduction, and leads quite rapidly into basic encoding and information theory and thence on to the basis of current encryption techniques. It outlines most of the presently used methods and gives some interesting examples. #ABSTRACT#348# Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188) #ABSTRACT#349# Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188) #ABSTRACT#350# This report details the development of a guard to monitor electronic traffic between two computer systems. The guard is intended to operate between two computer systems that are accredited to operate at different security levels. One system (the high system) must be accredited to process all information on the other system (the low system). The purpose of the guard is to automate the delivery of information from the low system to the high system while preventing any flow of information from the high system to the low system. #ABSTRACT#351# This paper describes in some detail the way in which Gould have incorporated security into their C2 level UNIX system. Support is based on integrity domains. It is stated that the mechanisms will also support the security labels etc needed for higher levels, but these details are 'topics of later presentation'. Their protected domains are in fact subtrees of the filing system. A restricted process cannot 'see' outside its domain. Common facilities are handled by a privileged trusted domain containing 'trusted servers' accessed via 'secure sockets'. The 'setuid' facility, whereby a process can activate a more privileged subtask, is abolished, so all privileges must be passed down the hierarchy. #ABSTRACT#352# This note proposes some standards for security features to be incorporated into UNIX. It is produced by Gould and AT&T, who are collaborating. They suggest that, as other manufacturers are also producing secure UNIXes, there is an opportunity for standardisation. The document makes some useful suggestions. However in a lot of cases, especially 'difficult' areas, they simply say they will 'follow NCSC guidelines - details to follow later'. #ABSTRACT#353# This paper contains a great deal of mathematical notation and is therefore fairly hard to follow. The main point of it seems to be to retain the name 'Bell and LaPadula model' and applying it to a model which includes a lot of useful recent work. It probably has major political significance and little technical significance - it may allow people to use non-interference while persuading their masters that they are using 'Bell-LaPadula' which has been given official blessing. #ABSTRACT#354# Note: Introduction: In this paper, we will describe several interesting aspects of the development of a formal security policy model for a military command and control system. The command and control system is being built to meet the B3 division and class of DoD 5200.28-STD. This paper will discuss the real world issues involved in developing a useful and accurate model of a very complex security policy. The policy developed for our target application has several interesting features and consequently the model is interesting in several respects. The system has several policy elements that required some novel mathematical approaches. These will be explained in detail in later sections. The system development has a long history and there have been several other attempts to develop a satisfactory model of the policy. These attempts were unsuccessful because they attempted to model a very complex security policy through an instantiation of the Bell and LaPadula model (BLP). The paper is organized in the following manner. We will first discuss several of the unique policy elements. We will then discuss the modeling paradigm applied to this problem. This will be followed by a discussion of some of the formal techniques used in the model. Lastly, we will discuss some of the payoffs that resulted from this effort. #ABSTRACT#356# Note: This paper advocates the use of dual labels for data storage, in particular in the MITRE Compartmented Mode Workstation (CMW). The dual labels are a 'sensitivity label', which has hierarchical and non- hierarchical components, for use with mandatory access control, and an 'information label', which has a similar structure, containing classification, compartments, codewords and other markings. The purpose of this arrangement is to allow a 'container' (file) to have a different label to the information stored in it. The sensitivity label must dominate the information label. The information label of an empty file will start low, and move higher as more sensitive information is added. It is claimed that this arrangement is more flexible than single label schemes, and cites several possible uses. The scheme described appears to be workable, but it is not obvious that it is necessary to use a complex label such as this . The paper appears to be well-considered, but would require more detailed examination before a definitive judgement could be reached. One member of the audience claimed that this work was 'surprisingly similar' to a paper which he had presented at the 3rd ACSAC (1987), and requested that Graubart's subsequent papers should cite this. #ABSTRACT#357# This paper describes how a commercial database system - the MISTRESS relational DBMS running under UNIX - is being adapted to support an integrity lock scheme that uses cryptographic sealing to enable multilevel data to be handled securely. It assumes that the UNIX system itself is B-level secure, that a secure crypto is available, and that the DBMS is too big to validate but can be encapsulated. The problem of inference via Trojan Horse is not examined. #ABSTRACT#358# We explore two approaches to introducing noise into the bus-contention channel: an existing approach called fuzzy time, and a novel approach called probabilistic par- titioning. We compare the two approaches in terms of the impact on covert channel capacity, the impact on performance, the amount of random data needed, and their suitability for various applications. For probabilis- tic partitioning, we obtain a precise tradeoff between covert channel capacity and performance. #ABSTRACT#359# Note: This paper reports some results from research of which the goal, yet to be realised, is to capture ðperfectlyð the notion of non- interference. A further goal is to generalise ðperfectð noninterference as to allow a quantifiable amount (e.g. so many bits/minute) of interference. Gray begins by pointing out some problems with McCulloughðs ðrestrictivenessð generalisation of noninterference. These are: „ It does not preclude timing channels; „ It does not preclude a high event from interfering with the probability of occurrence of a low event; „ It cannot be relaxed to allow ða small amountð of interference. The aim of this paper is to address the second of these problems. The kinds of system considered here are those which are genuinely non- deterministic (as opposed to those which are under specified or what we would call loosely specified). Moreover, it is assumed that the system designer is using randomness for an explicit purpose, to give desirable properties such as fairness, prevention of denial-of-service, or security. Thus the designer must specify, and the implementor accurately implement, desired distributions. By way of motivation, an example is given of a system which satisfies McCulloughðs restrictiveness property, and yet, most of the time, the outputs accurately convey something about the inputs. The heart of the paper is the definition of a property called probability-extended-restrictiveness, or P-restrictiveness. This is a reformulation of McCulloughðs definition for a system model which associates a probability with a state-transition. The modified property is, very briefly, about the existence of corrections (inputs) for perturbations of states for which the probability of transiting to a final state equivalent to the unperturbed final state is the same as the original probability. It is emphasised that this is an interim and not a final statement of a desirable security-property. A simplifying assumption is made, that the correction must be a single event, not an arbitrarily long sequence of events. This means that P-restrictiveness is acknowledged to be too strong: it excludes some systems which are restrictive and do not exhibit probabilistic interference. A large example is presented of the use of P-restrictiveness to distinguish between secure and insecure uses of nondeterminism to solve a denial-of-service problem. Finally, the composability of machines with P-restrictiveness is not yet proved. A limited result is given that the composition of P- restrictive machines is P-restrictive if the machines are synchronised. Probalistic interference in nondeterministic machines can be exploited by trojan horses to reliably leak information to unauthorized users. This problem has been noted by other researchers but has not previously been addressed. We extned McCullough's restrictiveness to additionally prevent probalistic interference. Then, to illustrate the use of our extension, we devleop a nondeterministic system that solves a denial of service problem and use our definition to prove that the system is secure. #ABSTRACT#360# We describe a general purpose, probabilistic state machine model which can be used to model a large class of nondeterministic (as well as deterministic) computer systems. We develop the necessary probability theory to rigorously state and prove probabilistic properties of modeled systems. Then we give a definition of information flow security making use of this formalism. Intuitively, information flow security is the aspect of computer security concerned with how information is permitted to flow through a computer system. We prove that our definition of information flow security implies an information theoretic definition. Finally, we give a verification condition for information flow security and prove that it implies our definition of information flow security,. #ABSTRACT#361# This paper sets out a second order modal logic for reasoning about multilevel security in probabilistic systems. We present a possible world semantics and prove that the logic is sound with respect to it. The semantics is novel in treating probability measures themselves as possible worlds. We give a syntactic definition of security and show that the semantic interpretation of our syntactic definition is equivalent to an earlier independently motivated characterization, Probabilistic Noninterference ([14]). We also look at a syntactic representation of Gray's Applied Flow Model (a special case of McLean's Flow Model, given in [25]), and discuss the relation between these characterizations of security and between their usefulness in security analysis. We give a syntactic description of a round-robin server and sketch the formal proof of its security. #ABSTRACT#362# Note: The talk was a faithful presentation of the paper which outlines some of the work carried out by the Computer Systems Research Institute at the University of Toronto to produce a secure version of their UNIX-compatible operating system TUNIS. The authors have a prototype of Secure TUNIS. The authors claim that it is not possible to have a secure version of ðtraditionalð UNIX evaluated above B2. However, TUNIS is much more amenable to being made secure than UNIX, and the authors are going for B3 and above. The achieving of B3 is made possible because TUNIS has a simple structure and is written in the verifiable language Turing Plus. This is not the case with UNIX, which has a non-trivial structure and is written in C. The security model for the secure version of TUNIS is a modified version of the Bell and LaPadula model. It is not clear from the paper what these modifications are, but it is claimed that they are necessary to retain compatibility with UNIX. To make it possible to verify the operating system as being secure, the authors have identified a two- fold partition of the kernel. One part dealing with the security policy, called the security manager, and the other part dealing with the security mechanism. The security manager is a small, verifiable module through which all requests must pass. It has a three-fold action. First, it identifies events that would be caused by a request. It then gets the appropriate security information using the security mechanism. Finally, if everything is OK then it authorises the request and allows security mechanism to execute the request. What happens if everything is not OK is not made clear. The authors do not claim that the module has been verified and leave open the question of the correct operation of the security mechanism. All they say is that the problem of verification has been simplified as the security manager and the security mechanism can now be verified individually. Although this split is claimed to benefit verification, it is also claimed that it is detrimental to efficiency. This paper will be mainly of interest to those developing secure UNIX at B3 or above. #ABSTRACT#363# This paper describes the current (Summer 1986) state of development of the Gould Secure UNIX UTX/32S 1.0, how it was made secure and plans for enhancement to higher security categories. #ABSTRACT#364# Note: This paper is about the prevention of inference in certain types of statistical data, for example census data. For a readable introduction to the subject see [Denn82]. The paper gives an algorithm for determining the bounds that can be deduced for unknown entries in a two dimensional numerical table (of non-negative integers) with known row and column totals. On the basis of these bounds the possible threat of inference of other data can be determined. The paper does not contain anything of fundamental interest in security except perhaps the design of particular algorithms. In this paper we reexamine a problem of protecting sensitive data in an p by p table of integer statistics, when the non-sensitive data is made public along with the row and column sums for the table. We consider the problem of computing the tightest upper bounds on the values of sensitive (undicsclosed) cells. These bounds, together with tighest lower bounds (which can be efficiently computed [G], define precisely the smallest intervals that an adversary can deduce for the missing sensitive cell values. Small intervals compromise the security of the undisclosed data, and in some cases violate laws on public data disclosure. We showed previously [G] that each (upper and lower) cell bound can be computed ?(p?) time by a single network flow computation, but that the bounds are not independent so that only ?(p log p) upper bounds need to be computed in this (relatively expensive) way. That is, after ?(p log p) initial bounds have been computed, each of the remaining (possibly ?(p?) bounds can be computed in constant time. In this note we observe that the number of initial needed bounds can be reduced from ?( p log p) to 2p - 1, by exploiting a recent result of Cheng and Hu. #ABSTRACT#365# A flaw in an operating system that had apparently been verified using the information flow technique indicates that the approach, as it has been practised, is incomplete. The software tool that was used requires a specifications to have a format prone to cause errors, so that a modification of the design of the tool is needed. Moreover, the verification process was logically incomplete, because flow analysis of a version of the specification free of errors yields formulas that can be proved only via invariant properties. This observation leads to an integration of two techniques for verifying security. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 67-73 This paper, by an author from MITRE, draws attention to weaknesses of the HDM flow analysis tool, and inquires into why a security flaw in a design was not discovered by a formal verification process using that tool. Flow analysis is contrasted with consideration of invariants of state as a means of verifying security. State-invariant analysis alone is incapable of exposing covert channels. Two weaknesses are identified. Firstly, the security level of source and target of an information-flow must be explicitly supplied, since the tool is unable to deduce it. This means including it as an extra parameter in every function call. This is confusing and error-prone, since it is not always clear what is source and target, so there is a collection of 'rules of thumb'. Apparently, 'enhanced HDM' also has this undesirable feature, while a MITRE- developed flow analyser does not. Secondly, verification through proof of formulae generated by the flow analyser is alleged to be logically incomplete, since analysis of a specification corrected with regard to errors as above yields formulae which can be proved only via invariant properties which presumably are unavailable to or unused by the flow analyser. The security flaw was not discovered because an error of the first kind masked the fact that the system was able to enter a state (which an invariant property would have precluded) in which an illegal flow could occur. The paper concludes that flow analysis should be used as a guide to which state-invariants need proving. On the face of it this seems not unreasonable, but to get the most out of this paper one would appear to need a working knowledge of the HDM tool. #ABSTRACT#366# Note: The authorsð goal is given as ðcompositionalð verification: treatment of systems composed of concurrent processes. Guttman claims that trace-based approaches, in the style of CCS or CSP, provide powerful specification techniques, but CSP or CCS are hard to use as theories in current verification environments, where automated support is poor. (We think Edinburgh would dispute this claim, as there exists a proof tool for CCS.) The position is taken that specifications are theories and requirements are candidate theorems. Work is in hand to provide such support, but still at an early stage, so that the proofs described in the paper were performed manually. The paper begins by describing a trace-based approach to specification not unlike CSP. A possibly novel feature is the use of functions of ðhistoriesð to serve the purposes for which other approaches use state variables. The main part of the paper is a verification of the correctness of certain security-relevant features of the SCOMP hardware architecture. The verification of SCOMP actually performed was essentially about software, and made some assumptions about the behaviour of hardware. This work is an attempt to discharge those assumptions, but in turn seems to need some assumptions about software, which are said to be uncontroversial (that certain system data structures only get altered at certain times). There is a bus connecting CPU, devices, file system, paged memory, memory-resident process and page tables and a specialised memory-management unit, (SPM), developed for SCOMP. The SPM combines the functions of virtual address translation and access checking. The virtual memory mechanism applies uniformly to a wide range of objects: ðtemporary memoryð, filestore segments and devices. Correctness conditions are informally stated as: „ On access using a real physical address, the CPU or device is executing in ring 0, (most-privileged); „ On access using a virtual address, then 1. The access requested is amongst those permitted - that is, kernel software has stored in the process table a suitable ðdescriptorð. The availability and content of such a descriptor is the means used by the kernel to implement the security policy. 2. The accessing process is executing within the ring-bracket (i.e. with the privilege specified by the descriptor). 3. The data in the page-frame is an up-to-date copy of the appropriate data on filesystem disc. These conditions are formalised and two theorems are given which express satisfaction of the informal correctness conditions. Proofs are not given, nor an indication of the cost of proof. I must confess that I had difficulty in following the exposition in detail, and feel that the paper attempts to cram too much material into the space available. A treatment at greater length would be much better. Interesting nevertheless. #ABSTRACT#367# Software development environments help programmers perform tasks related to the software development process. Different programming projects require different environments. However, handcrafting a separate environment for each project is not economically feasible. Gandalf solves this problem by permitting environment designers to generate families of software development environments semiautomatically without excessive cost. The paper covers several topics including the basic characteristics of Gandalf environments, our method for generating these environments, the structure and function of several existing Gandalf environments, and ongoing and planned research of the project. #ABSTRACT#368# The paper compares the Bell and LaPadula, SRI/MLS and Non- Interference models, leading to the overall conclusion that non- interference is the most general system - but it is too new for there to be any real experience of using it. #ABSTRACT#369# The paper reports an investigation on the abstract model for the Honeywell Secure ADA Target (SAT); this is the highest Gypsy- expressed model for SAT. The investigation concentrated on the covert channels (which were defined as information transfer via non-data objects, viz. buffer size, device flags, passage of time) to see if they could be used in collusion to circumvent the Bell-LaPadula based security policy. Two approaches were used to look at the storage channels: SRI non- interference, and shared resource analysis. The SRI property is a version of the Goguen-Messeguer non-interference principle, and states that a subject is non-interfering with another subject if no action taken by the former can have any effect on the latter. A system is multilevel secure with respect to the SRI property if the levels form a partially-ordered set, and a subject is non- interfering with another whenever the level of the former does not dominate the level of the latter. Unlike Bell-Lapadula, the SRI model considers information to be transferred by the permission or non- permission to perform an operation; however, as current specification and verification methods do not reason about time, only storage covert channels are detectable. The shared resource approach requires enumeration of all shared resources that can be referenced or accessed by a subject, coupled with careful analysis of each of these to determine whether it can be used covertly to transfer information. A flow analyser has been developed from the Gypsy optimiser, and this can be used to build up a 'shared resource matrix' (SRM) whose rows are shared resources and whose columns correspond to the operational primitives; the entries of the matrix indicate the possibility of reference and/or modification. The matrix reveals areas in which the search for covert channels should be concentrated. The authors claim that the SRM method requires both experience and a devious mind. The paper describes the authors experience of these two approaches, and describes the channels discovered. Both methods were successful in finding covert channels, and are flexible enough to cope with variety of security policies. Both require skill in application, though limited automation may be possible. The authors state that the non- interference approach probably cannot be sufficient by itself, that the SRM might be, and that a combination of the approaches is likely to be sufficient. Much work is required to make the systems usable. #ABSTRACT#370# This paper develops and applies a non-interferance formalism of multilevel security to the Secure ADA Target (SAT) abstract model, and shows that the model is multilevel secure. An analogous formulation is produced to handle the type enforcement policy of the SAT machine, and generalisations and extensions of both formulations considered. #ABSTRACT#372# This report describes an investigation into the use of cache memories in capability architectures. A theory to describe the relationship between the size of cache and its efficiency is proposed. the use of a simulator to test the theory and compare various cache management policies is described, and the results obtained discussed. Conclusions are drawn as to the best caching strategy for the SMITE capability Computer. #ABSTRACT#373# Outlines in a hand-waving fashion and without much useful detail the results of an experiment in audit analysis by pattern recognition. #ABSTRACT#374# Note: This paper describes a project to build a security monitor which abstracts information about unusual activity by the users of a system, which may be an indication of abuse of that system, either by an intruder or by a legitimate user behaving in an illegitimate manner. Rather than using an audit log, which collects far too much information, the system builds up user profiles of statistical data about which services are used, from where, in what manner and at what times. #ABSTRACT#375# A formal model is presented that captures the subtle interacrion between knowledge, action, and communication in distributed systems. The standard notion of protocol by defining knowledge-based protocols is extended, ones in which a processor's action may explicitly depend on its knowledge. Also considered is what it means for a processor to follow an honest protocol, one where, intuitively, it only sends messages that it knows to be true. Defining these notions turns our to be surprisingly delicate. #ABSTRACT#376# MUSE is a verification system extending the SRI HDM toolset by providing a capability for proving invariants (viz. SSP, Star Property) and constraints. MUSE was developed to verify the RAP (a guard system); also used for MLO. Invariants are those properties that must be true in all states: MUSE allows one to prove an initial state secure, and then use induction. Constraints are the expression of relations between the states before and after a transition; these have to be proven for each transition. The tools added by Muse consist of parser, merge program (allowing independent module development), a formula generator and a theorem prover. The theorem prover is interactive since users (specification writers) often have a good idea how the proof should go. It produces and uses command files, which can be edited to prove new formulae and to support proof maintenance. Using these command files, a complete proof of RAP takes about 11 minutes on a VAX. Experience implies that there should be a theorem prover kernel which remains stable, with heuristic facilities running on top of this kernel. These facilities would change and grow to provide a gradually improving user interface, but these would not affect overall reliability. #ABSTRACT#377# To date, there have been no confirmed incidents of a computer virus that specifically targets OS/2 systems. However, the many DOS viruses loose in the land do present a real and present danger for OS/2 users since most OS/2 systems are capable of running DOS programs, including DOS programs that have been infected by a virus. This paper describes the danger to OS/2 systems posed by DOS viruses and suggests countermeasures that may be employed against viruses in the future. The information presented is based on a series of experiments conducted with various DOS viruses in a controlled OS/2 environment. Some prognosications are also offered as to the form OS/2 viruses may take when they are eventually created. A plea is made for the notion that security and antiviral features should be built into OS/2 and other advanced microcomputer operating systems as an integral component. #ABSTRACT#378# A new type of data dependency, the Domain Reduction Dependency is defined. Given a set of attributes over which a query is being made, this dependency allows one to more accurately predict the probability of release of sensitive statistics for that query than could have been done with table size alone. In addition, the properties of DRD's provide metainformation on the gain and loss of information within a lattice of queries through the addition or removal of attributes, from a query set. This increased formalism on information loss and gain may provide insights which will allow the construction of better techniques for protecting the security of future statistical databases. #ABSTRACT#379# In 1982, S.Akl and P.Taylor proposed an elegant solution to the multilevel key distribution problem, using a cryptographic approach. Since then, continuing research has been conducted to try to realize and simplify their scheme. Generally speaking, our paper focuses on two problems associated with the Akl/Taylor scheme. First, we propose a time-memory trade-off technique to overcome the problem in their scheme of requiring an extremely large memory space. Second, we propose an extended scheme that localizes within a small region as much as possible, the inserting/deleting problem associated with the Akl/Taylor scheme. #ABSTRACT#380# Note: A description was given of a scheme to decentralise the responsibility of key distribution to groups in a large distributed system. The scheme chosen, in essence, is to arrange a number of key centers in a tree structure. The key center responsible for providing a session key for a particular group communication session is that key center lowest in the tree which has all the communicating users as its descendants. It is claimed that this will decrease the load on the root node. The system produces secret keys and can authenticate and be authenticated by its users. The key paradigm is that of safe prime factors of very large numbers. A key center high in the tree can calculate the keys of all centers which are its descendants, so a successful attack on the root node would compromise the whole system. An attack on a subsidiary node compromises all of its descendants. On the other hand, no set of subsidiary key centers can conspire to compromise a higher node than then one which is the lowest ancestor of all of them. A proposal to remove the vulnerability of the system to root attack would be to remove the root (and in general all layers of the tree that do not serve the users directly). There then arises the necessity to establish a protocol to enable cross-branch key communication. It seems apparent that the system can address problems of key center traffic congestion in very large systems. The amount of information that needs to be stored at each key center is very small (a few numbers) as keys of descendant centers and users can be calculated at will. The problem of vulnerability of the root node is not solved. The initial key calculations have to be done somewhere, and there is always the probability of a security breach at that time even if the root node (and others) are subsequently removed. #ABSTRACT#381# This paper proposes two distinct cryptosystems based on Rabin's scheme. The first incorporates coding theory and provides encryption only. The second provides simultaneously both private encryption and digital signature for network users. In the cases where the second scheme provides only encryption or only digital signature, the scheme provides that the bit ratio between plaintext and ciphertext is 1:1, ie. equivalent to that of the RSA scheme. #ABSTRACT#382# This paper reports on an investigation of the security issues related to Ada runtime support. First, the need to use Ada features requiring runtime support is motivated. The paper then describes how the Ada Runtime Library in the development environment is transformed to become the Ada Runtime System in the operational environment. Key security requirements, such as protection of the runtime library in the development environment, and design of a security architecture in the operational environment are examined. The paper concludes that further research is required along with the actual development of trusted Ada Runtime Systems. #ABSTRACT#383# A classic paper; worth reading. #ABSTRACT#384# This report presents the specification of operations for a secure document handling system (SERCUS). The specification uses the Terry- Wiseman Security policy Model and therefore acts as an example of the modelling approach. The specification uses the mathematical notation Z, and consequently also acts as an example of the use of Z in specifying secure systems. However, it must be noted that an appreciation of SERCUS, the model and modelling approach can usefully be gained even if the formal specifications are not read. The Terry- Wiseman Model and its interpretation are given as an Annex to this report. #ABSTRACT#385# This paper formally describes the requirements for a demonstration of a secure electronic registry control system (Sercus) to be implemented using the security attributes of the SMITE secure capability computer. #ABSTRACT#386# Note: SMITE Ref: 1006. This paper provides an introduction to the SMITE approach to developing high assurance secure computer systems. This approach can be characterised by a formal method of modelling security policies which provides a suitable framework for defining security requirements, and kernel software which can implement the model concepts directly. The modelling approach is illustrated by an English overview of a model for military security. How SMITE solves the common problems of Trojan Horses and viruses by using a sophisticated Trusted Path is also explained. #ABSTRACT#387# This paper gives an outline of the ideas underlying the Modular Compilation System to be used in the SMITE secure computer. This system prevents users loosing track of which generation of source text gave rise to which object code, by binding both together into an abstract data object, called a module. Operations give access to the latest versions and require both to be updated together. Linking modules together to form an executable object is performed automatically, so it becomes impossible to forget to relink after updating a module. Configuration control and mixed language working can also be provided. #ABSTRACT#388# SMITE is an approach to computer security being developed by the Information Security Research Section of the Royal Signals and Radar Establishment in Malvern. The purpose of this leaflet is to increase the awareness of this work and show the ways in which it can help in the procurement of electronic information systems which have a requirement for multi-level security. #ABSTRACT#389# This paper describes the results of a simulation of some aspects of heap store management. The effectiveness of various schemes is studies for systems with variable sized requests and incremental garbage collection. #ABSTRACT#390# This paper presents a model of security for computer systems where it is essential that the confidentiality of the information is maintained. The model is introduced using a simple analogy, it is then defined formally and its use illustrated by examples. The framework for using the model to achieve high assurance implementations of high functionality systems is also discussed. #ABSTRACT#391# This memorandum gives a users guide to the ADPOP compiler-compiler. ADPOP (Attribute Directed Parse in One Pass) has been developed primarily for SMITE Microprogram development, and runs on PerqFlex using Ten15. An outline of the history of ADPOP is given as well as a complete description of the syntax and examples. #ABSTRACT#392# Note: A quick and reasonably accessible summary of IS 7498-2. 7498-2 should be referenced if any reliance is to be placed on individual details, however. #ABSTRACT#393# A report on work to develop a separation kernel using GYPSY largely based upon Rushby's ideas. This is a move towards a highly trusted reduced functionality system which can be constructed using current state of the art techniques while providing a basis for useful applications. This work is being done at DODCSC and is attempting to remedy some severe deficiencies in the trusted computer system evaluation criteria which are pointed out in this paper. 1T7. #ABSTRACT#394# An interesting idea which provides an enhancement to a simple password scheme. It is a simple challenge-response system which follows a normal password entry. It might provide better security than a simple password but I suspect that in practice the algorithm will become well known and thus worthless either because it remains the same for a very long time or because the method of distributing the new algorithms to the users is not well protected. #ABSTRACT#395# This monograph has been superceded by the book of the same title. #ABSTRACT#396# This book introduces the specification notation Z by presenting a series of worked examples of the use of Z. As well as introducing Z the paper demonstrates a style of specification that consists of formal text, to provide a formal specification, and natural langauge text which introduces and explains the formal parts. This approach results in the production of readable specification. A glossary of Z notation is included. #ABSTRACT#397# This paper introduces the Security Model Development Environment (SMDE); a suite of prototype tools for the development of secure systems. The development of the SMDE was performed under contract for the Rome Air Development Center and Strategic Defense Initiative. The SMDE is based on a methodology for the construction and analysis of security models, which supports the model developer via an iterative model design process. The methodology supports a concept of automatic rule base generation which required the development of the prototype tools and the Common Notation for the expression of security models. The prototype tools are the Model Translator Tool (MTT) and the Testbed. The MTT automatically generates a rule base from a security model and the Testbed simulates the activity of a system using a model's rule base. The methodology, together with an extended model description, provides support for the automated tools and the impact of the methodology on security model development is summarized. The SMDE provides an iterative modeling approach that increases the productivity of model designers, simultaneously causing the model development process to be more accessible. #ABSTRACT#398# This paper discusses the relationship between the high cost of trusted computing and the way security requirements are stated in Request For Proposals (RFP's). This is done by introducing four types of trusted computer systems: Evaluated, Accredited, Tailored and Customized. These types of trusted systems along with their associated costs are discussed in detail and it is shown how systems transition from one type to the next. Finally, examples are given of how misstated or conflicting security requirements in RFP's lead to the development of each of these types of systems, thus driving up the cost of trusted system acquisition. #ABSTRACT#399# Before the advent of formal verification techniques, penetration attacks were the best way of establishing a degree of assurance in the correct operation of the security controls of a computer system. Even now, such attacks provide a way of checking the completenes of a formal specification and verification. This paper is a description of a successful penetration exercise, carried out, with permission, by a group of students on the main university computer. The SDC 'Flaw Hypothesis methodology' was used, which centres on a three stage cycle for locating faults. Stage 1 consists in hypothesising flaws, using historical weaknesses and the experiences of the team; stage 2 filters the hypotheses to see if the flaws exist. Stage 3 completes the cycle by seeing if flaws found are representative of more general design weaknesses. The attack reported in the paper was successful: for example (and most seriously) certain system subroutines did not fully check their parameters, and so a sequence of operations could be done to boost a user process to supervisor status (thus bypassing all further security checks). Other faults found included passwords being left in shared memory, and the existence of a way of causing the supervisor to loop indefinitely. One of the main conclusions is that for 'reasonably secure' systems, it is better to concentrate effort on penetration detection rather than patching flaws to prevent attacks succeeding #ABSTRACT#400# Note: This paper is concerned with the security-related issues of a network security monitor in a single broadcast LAN environment such as Ethernet. The paper formalises the possible attacks on the network. It then goes on to describe the basic strategy used in the network monitor, and how the monitor performed. The paper formalises an attack on the network into three phases, the preparation phase, the attack phase, and the post-attack phase. The network security monitorðs strategy is to build up a profile of the usage of network resources and then compare the current usage with the previous history to determine possible security violations. Once a security violation has been identified the location of the security violation can be discovered by refining the resolution of the monitoring in a hierarchical fashion (e.g. going from gateway, to workstation and finally to a specific user). Overall the paper provides a broad description of a network monitor and its function. The study of security in computer networks is a rapidly growing area of interest because of the proliferation of networks and the paucity of security measures in most current networks. Since most networks consist of a collection of inter-connected local area networks (LANs), this paper concentrates on the security-related issues in a single broadcast LAN such as Ethernet. We formalise various possible network attacks. Our basic strategy is to develop profiles of usage of network resources and then compare current usage patterns with the historical profile to determine possible security violations. Thus, our work is similar to the host-based intrusion- detection systems, such as SRI's IDES[9]. Different from such systems, however, is our use of a hierarchical model to refine the focus of the intrusion-detection mechanism. We also report on the development of our experimental LAN monitor currently under implementation. Several network attacks have been simulated and results on how the monitor has been able to detect these attacks are also analyzed. Initial results demonstrate that many network attacks are detectable with our monitor, although it can surely be defeated. Current work is focusing on the integration of network monitoring with host-based techniques. #ABSTRACT#401# Intrusive activity is occurring on our computer systems, and the need for intrusion detection has been demonstrated. This paper discusses some of the benefits and drawbacks of trying to detect the intrusive activity by analysing network traffic. A general solution, based on detecting and analysing abstract objects, is formulated. Finally, results from applying the solution are presented. #ABSTRACT#402# This is a general survey mainly of the interactions of databases and operating systems. There is also some discussion of hardware back-end processors. Not very accessibly presented. #ABSTRACT#403# The OSI standards have been built upon the the framework of the ISO 7 Layer Reference Model, for which a full tutorial is presented. In following this model, the book enables the reader to become familiar with the unifying strategy of OSI. Special attention is paid to the standards concerned with the upper four layers of the model which specify how computer systems cooperate to support complex applications over basic data networks. FTAM and X.400 (MOTIS) are discussed in separate chapters, whilst a further chapter contains fully worked examples of OSI operation in a step-by-step diagrammatic form. #ABSTRACT#404# This long paper gives a comprehensive survey of the issues involved with capability based architectures, considering their advantages and disadvantages. Examples of the approach taken by the practically implemented capability schemes are given in each area. #ABSTRACT#405# Note: This is a description of a practical system using encrypting network interface units. The interfaces are big and presumably expensive, and appear to have a lot of code in. Evaluation might therefore be a significant effort. #ABSTRACT#406# One of the overwhelming problems that software producers must contend with is the unauthorized use and distribution of their products. Copyright laws concerning software are rarely enforced, thereby causing major losses to the software companies. Technical means of protecting software from illegal duplication are required, but the available means are imperfect. We present protocols that enable software protection, without causing substantial overhead in distribution and maintenance. The protocols may be implemented by a conventional cryptosystem, such as the DES, or by a public key cryptosystem, such as the RSA. Both implementations ar proved to satisfy required security criteria. #ABSTRACT#407# This paper explores the issues of SneakerNet (S-Net), the term often used to describe the transfer of removable media from system to system. It offers a description of S-Net, examples of how and why it exists, and types of problems which can result. S-Net identification, threat analysis and negation, and documentation is developed. Finally, results and conclusions of a case study using a single large computer facility are shown. #ABSTRACT#408# Note: This paper deals with the problem of inference, of more-highly- classified data from aggregation of less-highly-classified data, in databases. The author distinguishes between two kinds of inference. The first kind is called cardinality aggregation. For example, the phone- book as such may be more highly classified than any name-and-number within it. Having given a name to this kind of inference, no more is said about it. The second kind is called inference aggregation. An example is as follows: suppose the information is classified about which company works on which project. Unclassified information is available about companies, employees, meetings and projects, and also the unclassified relations company-employs-employee, employee-attends-meeting, meeting-is-convened-by-project. From the available unclassified information, can a plausible inference be made about which company works on which project? From our knowledge of the real world, we would probably say yes. The paper advocates a method of detecting such paths of inference, based on drawing graphs which are called semantic networks. As far as I can tell, the situation envisaged is where the database relations are entirely ad-hoc, perhaps having grown in an ad-hoc way over time, and the analysis to be conducted is after the fact. The author seems unaware of, or at least makes no reference to, the mainstream ideas in relational database, such as data modelling, the entity- relationship-attribute class of models or Codd's extended relational model. These, together with integrity constraints are intended to capture the semantics of the database pretty fully. Thus in the example above, if one could deduce with confidence something about the company-works-on-project relation, the database designer ought to have included an integrity constraint. I will stick my neck out and assert that the best modern practice in database design should be to make all such possible inferences explicit from the schema and integrity-constraints. The author suggests means of analysing inference graphs, and the idea of testing possible inference by seeing whether any data is returned from specially-designed queries. He also suggests adding, for this purpose 'catalytic' data, which might represent common knowledge in the real world. In summary, this paper, although pedestrian in presentation, is thought-provoking. It points up the fact that existing security-models assume that any piece of data can be classified independently of any other. Thus there is a confusion, not yet resolved, between a classified piece of paper and a classified fact. Further, we don't yet have good models for systems which enforce invariants of state. Makes seven contributions to security aggregation research. It identifies inference aggregation and cardinality aggregation as two distinct aspects of the aggregation problem. The paper develops the concept of a semantic relationship graph to describe the relationships between data and then presents inference aggregation as the problem of finding alternative paths between vertices on the graph. An algorithm is presented for processing the semantic relationship graph to discover whether potential inference aggregation problems exist. A method of detecting some aggregation conditions within the DBMS is presented which uses the normal DBMS query language and adds additional catalytic data to the DBMS to permit a query to make the inference. The paper also suggests use of set theory to describe the aggregation conditions and the addition of set operations to the DBMS to permit the description of aggregation detection queries. #ABSTRACT#409# This paper suggests the trusted server as a means of injecting multilevel security into applications such as command, control and intelligence systems. It presents an example trusted database server and a trusted gateway server. A taxonomy is presented for gateway servers. Finally, the paper argues that the trusted server is a gap filler, in that it can off load much of the security design, maintenance and distribution complexity from client systems by permitting lower evaluation level clients to be used with the trusted server bearing much of the cost of multilevel security. #ABSTRACT#410# This classic paper shows a programming structuring method based on the concept of parallel composition of communicating sequential processes. A syntax is presented for a set of suitable primitive program constructs, incorporating developments based on those of Dijkstra. #ABSTRACT#411# This book supercedes, expands and illustrates the ideas of the earlier paper with the same title. A process is defined as an abstraction of the interactions between a system and its environment, and it is shown how 'traces' (sequences of actions) record the behaviour of processes. Systems consisting of multiple processes are then introduced, and then the concept of nondeterminism. The theme is developed to consider interprocess communication and shows how systems involving resource sharing can be structured and implemented using the CSP methodology. The book ends with a discussion of alternative approaches and the motivation for the CSP approach. #ABSTRACT#412# This 1980 Turing Award Lecture by a compiler expert discusses how various languages have grown during design and standardisation into monsters that are too big to be sure that compilers work; in particular, he advises that ADA is unsuitable for use in control systems for missiles or other such tasks where reliability is essential. #ABSTRACT#413# This paper points out the differences between traditional risk assessment, which is concerned with accidents, and security where violations are deliberate. It considers the problems, and concludes that the assessment process is still necessarily rather intuitive and should not be automated too hastily. #ABSTRACT#414# This paper proposes a new approach, SPI, for adding security to existing systems. Security functions are added in series to existing I/O paths without modification to the host system internals. The result is an I/O pipeline of security functions which is adaptable to both trusted and untrusted environments. Security of the physically separated SPI architecture is easier to analyze than other security products. Additionally, SPI requires no modification to the operating system. However, SPI is limited to the host processor interfaces. The SPI approach is compared with and contrasted to other ongoing security pipeline research. Examples of applications are presented which illustrate how security functions are added in a pipeline. These include a rogue program controller and intrusion detection systems. #ABSTRACT#415# Note: This paper chooses UNIX as a representative, widespread, insecure operating systems, and describes the security features it provides.. It then discusses a number of ways in which exploitable loopholes appear in operating systems, and how such loopholes circumvent the security mechanisms. #ABSTRACT#416# This book introduces local area networks and describes their position with respect to the OSI basic reference model and related standards (the physical, data link and network layers in particular). A number of local area network architectures are surveyed (including, Ethernet, Hubnet, Floodnet and binary routing networks), and more detailed examples are given in sections on the IBM token ring, the SILK register insertion ring and the Tornet 'multimode' ring. A chapter on the Cambridge Ring and its protocols then serves to introduce the main subject of the authors' expertise. The hardware and software used to interface computers to the ring at Cambridge is described in some detail and the Cambridge Model Distributed System is then taken as a local network case study, including an evaluation of its performance. The design and implementation of a high-speed ring network, based on the Cambridge Fast Ring is then described. The book is concluded with an evaluation of the flexibility and use of local area networks. There is a brief but informative suggested reading list at the end. #ABSTRACT#417# A cascade problem exists in a network of computers when data of a security level d can be passed to a user with a lower security clearance u elsewhere on the network without having to defeat any single component of the system that has an accreditation range great enough to allow users of level u and data of level d on a single system. An algorithm of time complexity order O(an3) and space complexity O(an2) is given to solve the cascade detection problem. Also the cascade correction problem, to remove all cascading paths from a network for a given cost, under restrictive conditions is shown to be NP-Complete. #ABSTRACT#418# This book considers aspects of computer security under various headings such as physical, operating system and database. Each section has an introductory tutorial section presenting the issues, followed by an extensive annotated bibliography giving 'original' papers and those which were state of the art in 1978. 1T60. #ABSTRACT#419# This paper gives a brief technical review of research in the areas of operating system security, as it was in 1978. It is mainly derived from an ACM book by the two authors entitled 'Computer security'. 1. #ABSTRACT#420# This paper describes the lattice scheduler. The lattice scheduler is a process scheduler that reduces the performance penalty of certain covert channel countermeasures by scheduling processes using access class attributes. The lattice scheduler was developed as part of the covert channel analysis of the virtual machine monitor security kernel for the VAX architecture designed to meet the requirements of the A1 rating from the National Computer Security Center. #ABSTRACT#421# This paper describes fuzzy time. This is a collection of techniques that reduces the bandwidths of covert timing channels by making all clocks available to a process noisy. Developed in response to the problems posed by high-speed hardware timing channels, fuzzy time has been implemented in the VAX security kernel. The VAX security kernel is a virtual machine monitor security kernel for the VAX architecture designed to meet the requirements of the A1 rating from the National Computer Security Center. #ABSTRACT#422# Considers whether Orange Book is applicable to databases, and concludes that not enough is known about database security yet in order to say, but it probably isn't completely applicable as it stands. #ABSTRACT#423# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#424# The rapid expansion of computer security information and technology has included little support to help the security officer identify the safeguards needed to comply with a policy and to secure a computer system. Los Alamos is developing a knowledge-based computer security system to provide expert knowledge to the security officer. This system includes a model for expressing the complex requirements in computer security policy statements. The model is part of an expert system that allows a security officer to describe a computer system and then determine compliance with the policy. The model contains a generic representation that contains network relationships among the policy concepts to support inferencing based on information represented in the generic policy description. #ABSTRACT#425# Pollyanna is a simple secure DBMS which utilises polyinstantiation. It has been designed and implemented to illustrate the problems which may be encountered when applications are built on top of a polyinstantiating DBMS. The implementation comprises a front end to a standard commercial RDBMS. The front end performs query modification and result filtering to achieve security. This document describes Pollyanna, the front end software and some of the problems which arose during the design of the system. #ABSTRACT#426# IEEE 802.1 'Overview and Architecture' describes in part a) the relationship between the standards, and their relationship to the OSI basic reference model. Three layers are defined: logical link control (LLC), media access (MAC) and the physical layer. The LLC part presents an OSI link layer interface and is common to each of the physical standards. The MAC part is media dependent and so is included in each of the physical standards. The physical layer coincides with the OSI physical layer: each different medium having a its own standard. Successive parts deal with addressing and management; architecture and internetworking. IEEE 802.2 defines the Logical Link Control services LLC1, LLC2 and LLC3. Each of these is based on the MAC service, which is a basic service giving sequencing, non-duplication and error detection, but not acknowledgement or flow control. LLC1 is a minor extension of MAC. LLC2 is a slightly generalized form of X.25 level 2's LAPB (i.e. HDLC) and is connection orientated with a destructive reset, flow control by the receiver and full error recovery by retransmission. LLC3 is based on a General Motor's protocol, being a slight enhancement of MAC to include acknowledgement. IEEE 802.3, 802.4, 802.5 and 802.6 describe the physical layer for various different network types. The first three are respectively CSMA/CD (Ethernet type), token bus and token ring networks. The last is for a 'Metropolitan network', a broadband system. #ABSTRACT#427# This paper presents the design and implementa- tion of a real-time intrusion detection tool, called US- TAT, a State Transition Analysis Tool for UNIX. This is a UNlX-specific implementation of a generic de- sign developed by Phillip A. Porras and presented in [Porr92B] as STAT, State Transition Analysis Tool. State Transition Analysis is a new approach to repre- senting computer penetrations. In STAT, a penetra- tion is identified as a sequence of state changes that take the computer system from some initial state to a target compromised state. In this paper, the development of the first USTAT prototype, which is for SunOS4.1.1, is discussed. US- TAT makes use of the audit trails that are collected by the C2 Basic Security Module of SunOS, and it keeps track of only those critical actions that must occur for the successful completion of the penetration. This ap- proach differs from other rule-based penetration iden- tification tools that pattern match sequences of audit records. #ABSTRACT#428# The architecture for an Embedded Secure Database Management System (ESDBMS) applicable to Command, Control, and Communication environments is presented. The ESDBMS design consists of three major components: 1) the GEMSOS tamperproof security kernel 2) an Embedded System Run-time Executive, and 3) the Trusted ORACLE RDBMS. The ESDBMS is designed to support a fully-functional DBMS while meeting high assurance requirements. Future enhancements to the basic version of the ESDBMS are identified which will broaden its applicability. #ABSTRACT#429# This is the official ISO definition of the 'seven layer' model. ISO have attempted to define a generalised but complete list of services for 'open systems' intercommunications (OSI). ISO 7498 does this by categorising these services into seven 'layers' the concept of which it defines first. The description of how these layers were chosen (given in an annex), provides an excellent introduction to the layers for a novice. The model has been enhanced by the addition of two addenda, ISO 7498/DAD1 and ISO 7498/PDAD2. The first of these defines the slightly modified services that are associated with connectionless (CL) rather than connection orientated (CO) communication and the second deals with security services at the various layers. Subsequent ISO standardization has resulted in standard services and protocols dealing with each of the layers. In time each of these layers will have associated or modified standards dealing with the topics presented in the addenda, but at the moment (Oct 86) insecure, connection orientated work prevails. Further related standards are also relevant: Services: Data Link Layer - ISO/DP 8802/1; Network Layer - IS 8348; Transport Layer - IS 8072; Session Layer - IS 8326; Presentation Layer - ISO/DP 8822; Application Layer (CASE) - ISO/DIS 8649/x. Protocols: Data Link Layer - ISO/DP 8802/x; Network Layer - ISO/DIS 8473; Transport Layer - IS 8073; Session Layer - IS 8327; Presentation Layer - ISO/DP 8823; Application Layer (CASE) - ISO/DIS 8650/x. #ABSTRACT#430# This addendum to the basic reference model defines the general security-related architectural elements applicable when protection of communication between open systems is required. It establishes, within the framework of the Basic Reference Model, guidelines and constraints to improve existing standards or to develop new standards in the context of open systems interconnection in order to allow secure communications. In order to accomplish these stated aims it defines a number of security relevant services and proposes mechanisms by which these services could be realised. It presents a matrix to show which mechanisms are appropriate to which services. It explains the relationship between services and mechanisms and the layered model, and the placement of security services in the actual layers of the basic reference (seven layer) model. Appropriate mechanisms are given for each. It concludes with a matrix showing the layers in which each of the services could be provided. The document concludes with consideration of the management of security: authentication management, access control management, and key management in particular. Two annexes give some background information on security in OSI (a reasonably long tutorial), and the justification used for security service and mechanism placement. At the beginning of the document a number of useful security related terms are defined (which are all used in the text).Superseded by T777 #ABSTRACT#431# Note: Supersedes #ABSTRACT#432# This paper describes the design of a prototype intrusion detection system for the Los Alamos National Laboratory's Integrated Computing Network (ICN). The Network Anomaly Detection and Intrusion Reporter (NADIR) differs in one respect from most intrusion detection systems. It tries to address the intrusion detection problem on a network, as opposed to a single operating system. NADIR design intent was to copy and improve the audit record review activities normally done by security auditors. We wished to replace the manual review of audit logs with a near realtime expert system. NADIR compares network activity, as summarised in user profiles, against expert rules that define security policy, improper or suspicious behaviour, and normal user activity. When it detects deviant (anomalous) behaviour, NADIR alerts operators in near realtime, and provides tools to aid in the investigation of the anomalous event. #ABSTRACT#433# Note: The treatise of the talk was that developing computer security is hard. This is, of course, a not entirely new concept to most of the community. The perception that increasing determinism (i.e. taking design steps) will tend to conflict with maintaining usersð ignorance of aspects of the systemðs behaviour has been around, certainly in the UK community, for some time. What the author has, I think, succeeded in doing is to make more precise this intuition and to pin-point the sources of the problem. This should, in principle, help suggest ways around the problem. Alas the paperðs tone in this respect was not one of great optimism. By way of example it showed that one ðobviousð strategy for refining a system failed. Trying to fix up one information flow often messes up another. The author refers to the security orderings, denoted ð, introduced previously by him and points out that ð and = are fundamentally different and should not be confused (but frequently are). Recall that = is the CSP satisfaction relation that is essentially about removal of non-determinism. Another way of putting this is that information flow properties are predicates on the space of processes whilst safety properties are generally expressed as predicates on the space of traces of a process. The mathematical content of the paper is high. #ABSTRACT#434# Note: Jacob uses the traces model of CSP to model what a user can deduce about the behaviour of other users from his observations and knowledge of the capabilities of the system. With this framework he defines a number of security orderings on systems and goes on to define a restriction on information flow. In more detail, he treats the system as a CSP process, and defines a set of events that represents the events a user may participate in, ie the 'window' through which the user can observe part of the system's behaviour. He then defines an infer function for a user for an observation. From these definitions, Jacob constructs a number of security orderings on systems. He then defines the restriction of information flow on the system, which can be paraphrased as follows: a. any possible observation that B might make can be explained purely by a trace of events about which B is permitted to know; or, turned round, b there is no possible observation l that B can make that could only be explained by the occurrence of an event (or events) that B is not permitted to know about. Jacob's formulation was criticised by McCullough on the following grounds: it does imply that the 'low' observer u cannot rule out the possibility that the 'high' user v did nothing but it does not prevent u narrowing down the range of possible behaviours of v. McCullough has devised an interesting example of a system that satisfies Jacob's restriction of information flow but is clearly highly insecure - see either McCullough's paper or the review of it in this report. A version of integrity that is dual to the restriction of information flow can also be described in this formalism, rather as one of the Biba policies is given as the dual of the Bell/LaPadula model. Jacob then goes on to describe what he has called 'security specifications'. These are generalizations of the infer functions defined previously. Whereas the restriction of information flow defined using infer functions allowed only the specification of either no flow or total flow between windows, these specifications can allow partial flows. These specifications form a lattice. This paper gives a security and specification-oriented semantics for systems. The semantic model is derived from that for the trace model of Hoare's Communicating Sequential Processes and is used to define various security concepts, such as multi-level secure systems, trusted users and integrity. An indication is given of how implementations of secure systems may be derived from their specifications. #ABSTRACT#435# Without going into detail, the paper describes the various steps in the design and verification of a 32-bit microprocessor chip. While not using the latest tools - the work reported was completed in 1983 - it is an interesting description of a real-life large-scale verification project, illustrating what is feasible in hardware verification. #ABSTRACT#436# Note: This paper describes a synchronisation mechanism for replicated databases which is claimed to require only a small amount of trusted code but is both fast and secure. The good performance of this mechanism is claimed to be a significant advantage compared with kernelised databases. The method described appears to be flawed in that it works for a strict hierarchy but not for a general lattice. In a replicated database a separate DBMS (or container) exists at each classification level. The container at each security level contains data at that level and also copies of all the data at lower levels. When a data element is updated the update must be copied to all dominating containers to maintain consistency. The paper is concerned with achieving consistency while at the same time preserving security. Two plausible but incorrect solutions are outlined to illustrate the problems involved. These are followed by a ðcorrectð solution, which as I remarked above I believe to be flawed. The first incorrect solution makes use of a two phase Commit protocol. The container at the security level of the change is updated but does not commit. Next all dominating containers are updated. Finally, if all the updates have failed all are aborted. This can cause a covert channel if one of the higher level DBMSs aborts deliberately. The second incorrect solution involves the TCB executing the transaction on the container at the security level of the transaction as before. This time the transaction is committed and only then are updates propagated to all dominating containers. This is secure but does not guarantee one copy serialisability - hence inconsistencies can occur. The ðcorrectð solution is essentially a tightening up of the second example above. Each untrusted DBMS follows a strict ordering protocol in taking requests from and returning responses to the TCB. This protocol gives consistency but not security and so it does not need to be trusted. On receiving a change request the TCB commits the change at the level of the transaction. Dominating containers are then updated one by one according to what is described as a ðtopologicalð ordering of the security lattice. The idea is explained by saying that the order of updates is such that the security level of each container in the update chain dominates the security level of the previous container. However this implies that the security lattice can be totally ordered, which is, in almost all cases, impossible. It may well be that the algorithm could be refined to take account of this problem, but this will be at the cost of complexity in the trusted code. The paper is only worth reading if the reader is working directly in the replicated database area and even then it should be treated sceptically. In a multilevel secure database management system based on the replicated architecture, there is a separate database management system to manage data at or below each security level, and lower level data is replicated in all databases containing higher level data. In this paper, we address the open issue of transaction processing in such a system. We give a synchronisation protocol such that it guarantees one-copy serializability of concurrent transaction executions, it is secure since the information always flows in one direction - from databases at lower security classes to databases with higher security classes, and it can be implemented in such a way the the size of the trusted code (including the code required for concurrency and recovery) is small. #ABSTRACT#437# This paper makes original contributions in two different areas related to the concurrency control in multilevel secure, multi-version databases. First, it explores the issue of correctness criteria that are weaker than one-copy serializability. The requirements for a weaker correctness criterion are that it should preserve database consistency in some meaningful way, and moreover, it should be implementable in a way that does not require the scheduler to be trusted. This paper proposes three different, increasingly stricter notions of serializability that can serve as substitutes for one-copy serializability. Second, it presents a multi-version timestamping protocol that has several very desirable properties: It is secure, produces multi-version histories that are equivalent to one-serial histories in which transactions are placed in a timestamp order, avoids livelocks, and can be implemented using single-level untrusted schedulers. #ABSTRACT#438# Note: There has been a spate of papers about MLS object-oriented DBMSðs recently. From a security point of view this is a slightly simpler problem than for general object-oriented systems because of the restricted nature of objects. An object-oriented database consists of a collection of objects containing a set of attributes. Each attribute has a value. Access to the attributes is by means of methods associated with the object. Examples of simple methods could be the operations of reading or writing values of attributes. A method is invoked by a message sent to an object (by another object). The success or failure of a method, along with other data, is returned to the invoker as part of the request. These objects are unlike the traditional objects of security in that they are active, i.e. they are really subjects, although they do preserve data. Attributes are equivalent to fields in a record. Methods are small programs. In this model, information can flow either when an object is created or when a message is passed between objects. In order to control information flow a message filter is proposed. Objects have a security class. Messages have a status, unrestricted or restricted. If a message is restricted then it may not affect the attributes of the destination object and the status of any resulting messages must also be restricted. Information flow is controlled in four cases: „ if the security class of a destination object is the same as that of the source there is no restriction; „ if the security class of a destination object is not related to that of the source no message may pass; „ if the security class of a destination object strictly dominates that of the source the method is invoked but the message filter returns the value nil so no returned data flows downward; „ if the security class of a source object strictly dominates that of the destination the message filter sets the status of the message to restricted so data can be read but not written. Timing channels are not controlled by this mechanism. Further restrictions are present when an object sends a message to itself. Since the system is object-oriented there are two other types of information flow to be controlled: „ class-instance flow where information flows from a class to its instances; „ inheritance flow where, if an object which inherits attributes and methods from an ancestor, the security class of the object must dominate the security class of the ancestor. The first case is controlled by the message filter because object creation is performed through messages. The second case is not controlled. Although this scheme was expected to be implemented on a secure machine with a conventional security kernel architecture it is expected that the filter could perform a security critical role. In this case, an object can have untrusted methods. In this case the message filter needs to know if any attributes have changed or prevent any attributes from changing, and enforce the restricted status of resulting messages. For a clearer exposition of an MLS object-oriented data model see [Lunt89]. However, use of the message filter to replace a security kernel, although currently undeveloped, is an idea worth watching. We present a new security model for object-oriented database systems. This model is a departure from the traditional security models based on the passive object - active subject paradigm. Our model is a flow model whos main elements are objects and messages. An object combines the properties of a passive inofrmation repostory with those of an active agent. Messages are the main insturment of information flow. The chief advantages of the proposed model are its compatibility with the object-orientated data model and the simplicity with which security policies can be stated and enforced. #ABSTRACT#439# In this paper we give a new decomposition algorithm that breaks a multilevel relation into single-level relations and a new recovery algorithm which reconstructs the original multilevel relation from the decomposed single-level relations. There are several novel aspects to our decomposition, and recovery algorithms which provide substantial advantages over previous proposals: (1) Our algorithms are formulated in the context of an operational semantics for multilevel relations, defined here by generalizing the usual update operations of SQL to multilevel relations. (2) Our algorithms, with minor modifications, can easily accommodate alternative update semantics which have been proposed in the literature. (3) Our algorithms are efficient because recovery is based solely on union-like operations without any use of joins. (4) Our decomposition is intuitively and theoretically simple giving us a sound basis for correctness. In this paper we also argue that some of the alternate update semantics which have been proposed for multilevel relations should be available as options, but should certainly not be made an integral part of the data model. #ABSTRACT#440# Note: This paper is a critique of (a slightly out of date) version of the SeaView multilevel relational data model. SeaView is probably the most extensively discussed multilevel database model. It is a product of some of the best US researchers in the field. One of the most significant and controversial aspect of SeaView is that it embraces polyinstantiation. This is where, to prevent covert information flows, a database stores different information about the same entity at different security classes ð the lower security class data can also be used to give cover stories. The paper explores three main areas of SeaView: „ the Inter-Instance Property, which is about the relationship between views at different classifications of a relation instance; „ the multivalued dependency (MVD) requirement of Polyinstantiation Integrity, which is required for consistency of updates; „ the correctness of the lossless decomposition of multilevel relations. The paper has already been overtaken by events for the suggested modification to the Inter-Instance Property. It has been incorporated into the latest version of the SeaView security model ([Lunt90]). As this paper shows in figures 4 and 5, the MVD in SeaView can result in a large proliferation of elements. Jajodia and Sandhu argue also that useful meanings can be assigned for instances of relations without the MVD requirement. However, these new instances admit different descriptions of an entity which are at the same classification where no decision can be taken as to which description is to be chosen. For decomposition of relations Jajodia and Sandhu use a more complete key and store null values in decomposed relations. Also they use natural joins rather than outer joins in the recovery. They argue that decomposition in SeaView has not been analysed as rigorously as other areas and that their use of natural joins considerably simplifies a very difficult area. However, even Jajodia and Sandhuðs decomposition work is not yet complete. Polyinstantiation integrity (PI) as defined in the Sea View multilevel relational data model consists of a functional dependency component and a multivalued dependency component. We show that the latter component rules out many practically useful relations and is therefore unduly restrictive. This leads us to propose that PI be defined to consist only of the functional dependecny component. For this revised definition of PI, we formulate and prove correct a lossless decomposition of multilevel relations into single level ones with recovery based on the natural join operation. #ABSTRACT#441# In this paper we give a formal operational semantics for update operations on multilevel relations, ie. relations in which individual data elements are classified at different levels. For this purpose, the familiar INSERT, UPDATE and DELETE operations of SQL are suitably generalized to cope with polyinstantiation. We conjecture that these operations are consistent (or sound) in that all relations which can be constructed will satisfy the basic integrity properties required of multilevel relations. We also conjecture that the operations are complete in that every multilevel relation can be constructed by some sequence of these operations. #ABSTRACT#442# SRI International's real-time intrusion-detection expert system (IDES) system contains a statistical subsystem that observes behavior on a monitored computer system and adaptively learns what is normal for individual users and groups of users. The statistical subsystem also monitors observed behavior and identifies behavior as a potential intrusion (or misuse by authorized users) if it deviates significantly from expected behavior. The multivariate methods use to profile normal behavior and identify deviations from expected behavior are explained in detail. The statistical test for abnormality contains a number of parameters that must be initialized and the substantive issues relating to setting those parameter values are discussed. #ABSTRACT#443# Note: This paper describes an attempt to extend the Yellow Book methods for security evaluation directly to network systems. The method is systematic and quite simple. However it may be too rigid to be useful in practice. The paper is quite short, so is probably worth a look! #ABSTRACT#444# Trojan horses, viruses, worms, and other malicious logic that seek to interrupt service or modify or destroy data are not necessarily defeated by confidentiality mechanisms. The Air Force Trusted Critical System Evaluation Criteria (AFTCCSEC) supplements confidentiality requirements found in the Trusted Computer System Evaluation Criteria (TCSEC) by addressing integrity and service assurance. This paper introduces and describes criticality division/class G2 found in the AFTCCSEC. The approach imposes mandatory controls including access constraints, type enforcement, detection techniques, and use of a resource scheduling architecture. It applies to all life-cycle phases: development, distribution, operations, and maintenance. Features include program/data isolation (eg. physical, logical or use of cryptography), protection against covert criticality channels (that allow malicious code insertion), and strict configuration control of software and hardware. Any TCSEC division.class and G2 criticality can coexist, though retrofit of G2 will require an existing TCSEC TCB of B1 or higher. This paper provides a basic understanding of the concepts and policy, and also addresses questions most often asked by reviewers of the AFTCCSEC document. #ABSTRACT#445# Air Force missions could be forced to fail by an enemy agent launching a malicious logic attack. These missions must be protected. Because of the imminent, potential danger, a protection approach has been developed that is easily understood and implemented for a minimum cost - because it uses Orange Book methods and mechanisms. The criteria for protection of critical systems are given as the G3 division/class of the Air Force Trusted Critical Computer System Evaluation Criteria (AFTCCSEC). #ABSTRACT#446# Note: This paper describes an attempt to extend the Yellow Book methods for security evaluation directly to network systems. The method is systematic and quite simple. However it may be too rigid to be useful in practice. The paper is quite short, so is probably worth a look! #ABSTRACT#447# StarOS is a message based, object orientated multi-processor operating system specifically designed to support large collections of concurrently executing cooperating processes. It is an object orientated system where all information is encoded and stored in typed objects. The type of an object determines the set of functions which can be performed on the object and hence the behaviour of the object. To access an object or alter information stored in it, a process invokes some function of the object's type. In order to do this it requires a capability for that object. It ran on a cluster of LSI-11s (up to 14) linked together by a memory mapping bus. The various clusters, of which there could be an unlimited number, were connected to inter-cluster busses by a processor in each cluster. A processor could map chunks of its 64K name space onto objects (i.e. load them into store) as long as the processor contained the relevant capabilities in its capability name space. #ABSTRACT#448# This note gives a summary and the current (mid 1986) status of each of four NCSC documents: the revised version of 'Trusted computer system evaluation criteria' (known as TCSEC or Orange Book), 'Security requirements for automated information systems (AIS)', 'Trusted network guideline' and 'Guideline on office automation'. #ABSTRACT#449# Note: This paper describes how two techniques proposed to increase reliability can be used to provide protection against attacks by computer viruses. It starts off by characterising a computer virus in reliability terms: it is a deliberate design fault; when triggered, the error it causes is a change in an executable file. The error in turn causes other errors in the 'normal' way it does in the case of a random fault (except with a virus the propogated errors are all of the same type). The two techniques suggested to counter the problem are the use of Program Flow Monitors (PFMs) which try to detect errors, and of n- version programming (NVP) which attempts to detect deliberate or accidental design faults before they can cause errors. PFMs are hardware-based mechanisms to check that the dynamic behaviour of a program is 'as expected' - for example, compilers and assemblers could generate signatures for each section of code without branches or subroutine calls, and the PFM could then be loaded with these when a program is run, generate its own version on the fly and check the actual matches up to the expected value whenever a control flow change occurs. NVP requires that n (greater than 2) versions of a program are designed and implemented independently from a common specification; all versions are then run concurrently on a multi-processor computer (or pseudo-concurrently on a single processor), with a consensus being required at certain points. (A weaker form would require them all to run together during a prolonged testing phase, with a randomly-chosen one being used thereafter, but this is susceptible to deliberate design flaws). Where either of the above techniques are required for reliability reasons, then to extend their scope to cover security is a sensible action. However, if security is the primary concern, then both techniques can substantially increase the cost of the hardware; in addition, neither technique is fully accepted within the fault-tolerance community, and in particular the virtues (or lack of them) of the NVP technique would appear (from the discussions that followed the presentation) to be the subject of much acrimonious debate. The applicability of fault tolerance techniques to computer security problems is currently being investigated at the UCLA Dependable Computing and Fault-Tolerant Systems Laboratory. A recent result of this research is that extensions of Program Flow Monitors and N- Version Programming can be combined to provide a solution to the detection and containment of computer viruses. The consequence is that a computer can tolerate both deliberate faults and random physical faults by means of one common mechanism. Specifically, the technique described here detects control flow errors due to physical faults as well as the presence of viruses. #ABSTRACT#450# The idea of using formal logic to reason about small fragments or single layers of a software/hardware system is well-established in computer science and computer engineering. Recently, formal logic has been used to establish correctness properties for several realistic systems including a commercially-available microprocessor designed by the British Ministry of Defence for life-critical applications. A challenging area of new research is to verify a complete system by linking correctness results for multiple layers of software and hardware into a chain of logical dependencies. This dissertation focuses specifically on the use of formal proof and mechanical proof-generation techniques to verify microprocessor- based systems. We have designed and verified a complete system consisting of a simple compiler for a hierarchically structured programming language and a simple microprocessor which executes code generated by this compiler. The main emphasis of our discussion is on the formal verification of the microprocessor. The formal verification of the compiler is described in a separate paper included as an appendix to this dissertation. Combining correctness results for the compiler with correctness results for the microprocessor yields a precised and rigorously established link between the formal semantics of the programming language and the execution of compiled code by a model of the hardware. The formal proof also links the hardware model to the behavioural specification of an asynchronous memory interface based on a four-phase handshaking protocol. The main ideas of this research are 1) the use of generic specification to filter out non-essential detail, 2) embedding natural notations from special-purpose formalisms such as temporal logic and denotational description, and 3) the use of higher-order logic as a single unifying framework for reasoning about complete systems. Generic specification, in addition to supporting fundamental principles of modularity, abstraction and reliable re-usability, provides a mechanism for enforcing a sharp distinction between what has and what has not been formally considered in a proof of correctness. Furthermore, it is possible to create generic specificaiotn in a pure formalilsm with the expressive power of higher-order logic without inventing new constructs. Natural notations from special-purpose formalisms offer the advantage of concise and meaningful specifications when applied to particular areas of formal description. Semantic gaps between different notation are avoided by embedding them in a single logic. Special-purpose rules based on these notations can be derived as theorems with the aim of implementing more efficient proof strategies. Finally, it is argued that the primary purpose of using mechanical proof generation techniques to reason about software and hardware is to support the intelligent participation of a human verifier in the rigorous analysis of a design at a level which supports clear thinking. 81122. #ABSTRACT#451# Most current trusted automated information systems do not allow changes to or extensions of the access control policy implemented by the system vendor. This closed approach to access control can restrict the operation of site applications and commercial off-the-shelf applications on trusted systems. This paper presents a flexible, open access control framework that provides relief from these restrictions. A network license mechanism is used to illustrate the problem and the applicability of the framework. #ABSTRACT#452# A capability is a precomputed access permission; it often viewed as a ticket, and in this case must be unforgeable. The paper claims that capability systems can be categorised by the answers to certain key questions, viz. what happens: when a capability is created (access rights might or might not be added); to the capabilities for a segment if the security aspects of that segment are altered (access rights might or might not be altered, or they could be flagged as needing change); when a capability is copied (access rights could be further restricted, set to some suitable maximum or correctly updated by software, or left unaltered); when a capability is prepared for access (access rights could be further restricted, set to some suitable maximum, or left unaltered); and, when the processor attempts to access something (no checks could occur, or access rights could be checked against available rights, or attempted access could be checked against the computed maximum rights)? Using this taxonomy, the differences between various proposed and existing capability systems can be drawn out. In addition, the paper shows by examination of the star property how the taxonomy can be used to check the suitability of a particular system for a given security policy. When the paper was presented to the IEEE symposium on Security and Privacy, a slightly different formulation of these key questions was used: when are basic access rights established; what is the timing of Discretionary Access Control; what are the limits on capability sharing; what is process of preparing to access; and, how expensive are runtime checks. #ABSTRACT#453# Note: Karger addresses how the Clark and Wilson data integrity model, first presented at the previous year's IEEE Security and Privacy Symposium, can be implemented on a particular secure capability architecture (SCAP). There are two techniques at the heart of the proposed implementation. The first is to enhance the capabilities to support tokens which identify who (or what) can use the capability and to prevent multiple use of a particular capability. The second is a proposal for Access Control List constructs to efficiently support the Clark and Wilson model. The proposed constructs are more complex than those found in currently available operating systems. The paper then goes on to briefly examine a range of related work and to compare it with Karger's proposals. Overall the paper covers a wide range of issues relating to integrity models, addressing none in any particular depth. The contents of the paper do not appear to be of immediate interest to the CESG Secure Distributed System work, although it should be of interest to anyone considering the problems of implementing Integrity policies. Examines the Clark and Wilson model for commercial data integrity and proposes an implementation based on the author's secure capability architecture. The paper shows how secure capabilities and protected subsystems are ideal for implementing commercial data integrity, but also raises areas where the Clark and Wilson model may have difficulties in actual use. The level of formal verification required appears higher than most commercial systems would be willing to try, and the user interface for specifying separation of duties appears extremely complex.. #ABSTRACT#454# Many discretionary Trojan Horse attacks can be defeated by a table- driven file name translation that has knowledge of the normal patterns of use of a computer system. File name translation is built into a protected subsystem, and the human user is queried about possible violations of discretionary access control policies. The technique is most effective against unauthorized tampering or sabotage and can be used in conjunction with non-discretionary security controls. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 32 - 37 Capability systems can in theory provide a great deal of protection to their users, but in practice they are rarely implemented in this way. For a variety of reasons, application and system programs are rarely constrained in their operation despite the fact that the technology was designed to do precisely this. The main reason for the lack of constraints on programs is the need for users to be able to refer to their files by name. This in turn means that the runtime environment for a program will provide a way of converting names - such as those the user may supply as parameters to the program - to capabilities; consequently, the program is not restricted to accessing just those files the user intended. Karger suggests that the standard command line interpreter, or 'shell', should be expanded to know - by means of tables - the expected file access activity of each program. By analysing the command line typed by the user to activate the program, and checking a file open request by the program against this analysis, the system will be able to detect unusual requests. The user could then be directly interrogated by the system, who would be able to permit or deny these requests. The scheme, operating purely on the basis of the names of objects, cannot enforce classification-based rules on the release of information, nor can it ensure that proper use is made of the objects that the program is expected to access; all it can do is to stop certain types of attempts to subvert the 'discretionary' (not label-based) controls. The scheme is thus suitable for providing an extra level of control on top of more standard mechanisms for implementing access controls, to give an added degree of assurance that the security policy and intentions of the users are not being subverted. #ABSTRACT#455# Note: The presentation opened with an explanation of why immediate revocation (of access rights) is necessary. The author explained that aside from the obvious advantage of revoking access rights at the earliest opportunity, immediate revocation is a prerequisite for immediate deletion of objects and that immediate deletion is required in order to prevent some types of storage channel in connection with storage quotas. He then went on to explain that in the past, difficulties had been encountered in implementing immediate revocation in operating systems such as Multics. These difficulties, and performance issues had been noted by the policy makers who had then stopped putting immediate revocation into their policies. Two current schemes for implementing immediate revocation, Revocation with Back Pointers (as used in Multics), and Redellðs Revocation with Indirection, were explained and the author then moved on to explain two new schemes. Revocation with Eventcounts and Revocation by Chaining. Basically, Revocation with Eventcounts makes use of Reed and Kanodiaðs eventcounts to keep track of whether a processðs access to an object is up to date. If it is not, then its access rights are re- computed. The author pointed out that this scheme was most applicable to systems that use shared page tables. Revocation by Chaining is only applicable in systems that have multiple page table entries for shared objects. The scheme involves adding an extra field to each entry. This extra field is used to link all of the entries for each object into a circular chain which the operating system can then follow relatively easily. #ABSTRACT#456# For those who understand capabilities, access lists and how to build operating systems, this paper describes how to build a machine which can use all the best features of both systems and has a chance of running acceptably fast. 1T2; T7. #ABSTRACT#457# This paper is a study of the covert storage channels found in disk I/O optimization schemes. It examines the source of the problems in the context of various disk architectures, proposes several classes of generic solutions and concludes with recommendations for future storage-system architectures. The work was done as part of the covert channel analysis for Digital's VAX security kernel. #ABSTRACT#458# Note: This paper was adjudged the joint 'Best Paper' at the symposium at which it was presented. It is required reading for anyone involved in designing systems based on Virtual Machine Monitors. It also provides an excellent example of a real, production quality, security kernel. The aim of the project was to develop a Virtual Machine Monitor (VMM) for the VAX Architecture. The VMM was to support the VMS and ULTRIX Operating Systems. The product was to take a step forward from the research quality security kernel implementations that have been developed over recent years and to develop a properly engineered production quality security kernel. The VMM is currently in the Design Analysis Phase of evaluation at NCSC. This paper gives an overview of the VMM. The original idea for this work was discussed in 1981. The paper acknowledges some fifty people who played a direct part in its development. It is a substantial effort. Steve Lipner, who heads the Security Group at DEC, said that DEC were not planning to offer the VMM as a commercial product. He said that this decision was a commercial judgement and not a technical one. He added that if the commercial situations changed then he saw no technical problems in offering the product. However, he also said that the market for A1 products was small and that US export restrictions effectively cut off some 50% of his potential market. This point came up again later in the conference and was clearly of serious concern to him. A VMM is not the same as a security kernel. However, the paper states that the requirements for A1 caused them to omit some features traditionally seen in Virtual Machine Monitors. The VMM is therefore primarily a security kernel and the paper tends to use the terms interchangeably. It was necessary to make a small number of changes to the microcode to virtualise the VAX architecture. These ensure that unprivileged code may not access the privileged state of the processor. All such attempted accesses are trapped. A further change to the Architecture is that the four rings available to an Operating System on a VAX processor are compressed to three on the VMM. This is achieved by concatenating the innermost two rings (executive mode and kernel mode) into one. This could cause problems if an Operating System running on the VMM had some inbuilt security features. However, the paper states that ULTRIX doesnðt make use of the distinction between the two modes and that VMS uses it only for reliability purposes. The security kernel is designed in layers with the usual rules that layers should only make use of facilities provided by lower layers. Each layer has no knowledge of higher layers. This abstraction is an excellent one to adapt from the point of view of modularity and simplicity. Unfortunately some aspects of security kernel cannot be described (sensibly) in this way. See the audit paper for an example of this happening and the ingenious solution (patch ?) used to get round it. Each layer is, in effect, a reference monitor in its own right since it has layer specific subjects and objects and a consequent need to mediate accesses. The approach to I/O is very different to the memory-mapped approach traditionally offered by DEC processors. The reason for this is simply performance. Each access to a CSR (control and status register) would need to be trapped by the VMM is the conventional method was adopted. Instead I/O is provided by a kernel call. This approach improves I/O performance dramatically but has the disadvantage that untrusted virtual device drivers need to be written for each Operating System running on the VMM. The VMM was coded in MACRO, PL/I and PASCAL. MACRO was used where enhanced performance was required. The authors remark that the switch from PL/I to PASCAL caused many bugs due to programmers misunderstanding the parameter passing mechanisms of the two languages. The switch was made because of the stronger typing offered by PASCAL and because a high quality PASCAL compiler became available during the project. The kernel contains 49K executable statements of which some 11K are in MACRO. DEC claim that performance is 30% to 90% of VMS performance depending on workload. DEC have given considerable thought to the design of the interface between the user and the TCB. The requirement for A1 demands simplicity and verifiability while the user wants a friendly, relatively sophisticated interface, which means lots of code. DEC have divided trusted user commands into two groups: Secure Server commands and SECURE Commands. The idea is that Secure Server commands should be the ones that the user is using constantly such as login, logout and connect/remove VM requests. SECURE commands are more administrative in nature and are more likely to be used by the System Manager, the Operators and the Auditor. However there is no prohibition on the ordinary user using SECURE commands. Secure Server commands are implemented in the conventional way by means of a trusted path invoked by a Secure Attention Key. SECURE commands are passed directly by the untrusted Operating System. The Operating System then invokes a kernel call to action the command. Before executing the command the kernel forces the user to hit the Secure Attention key and informs him of the command to be executed. The user can choose to proceed or abort. (Note that Figure 5 which is supposed to give an example, is missing.) The paper gives the impression that the A1 requirements for modularity, simplicity and layering were very strong influences on the design. Conversely the use of Formal Methods appears to be almost an afterthought. The language used is InaðJo. The FTLS is not yet complete but is expected to contain about 12K lines of InaðJo. This gives a ratio of 4:1 between FTLS and code compared with the often quoted estimate of 10:1. The Security Policy Model is, of course, based on Bell and LaPadula. The paper also discusses various aspects of the management of the system development process. It is interesting that the team are using the kernel itself as their development machine. They claim that this has helped to keep performance near the top of their list of objectives! Overall an excellent paper that should be read by all with a serious interest in security kernel design. Describes the development of a virtual machine monitor (VMM) security kernel for the VAX architecture. The paper particularly focuses on how the system's hardware, microcode, and software are aimed at meeting A1-level security requirements while maintaining the standard interfaces and applications of the VMS and ULTRIX-32 operating systems. The VAX security kernel supports multiple concurrent virtual machines on a single VAX system, providing isolation and controlled sharing of sensitive data. Rigorous engineering standards were applied during development to comply with the assurance requirements for verification and configuration management. The VAX security kernel has been developed with a heavy emphasis on performance and on system management tools. The kernel performs sufficiently well that all of its development is now carried out in virtual machihes running on the kernel itself, rather than in a conventional time-sharing system. #ABSTRACT#459# Note: This paper is virtually a sales pitch for a particular product (Intel's iKGM-100 key generation module, a NSA-endorsed CCEP device). It shows one way in which it can be used to provide network-layer encryption for a network of PCs by means of a special network interface card, operating as a coprocessor (for trusted systems) or 'inline' (in which case the encryption key defines the 'classification' of the running system). Key distribution is not addressed in the paper. #ABSTRACT#460# Currently there is a great deal of interest concerning polyinstantiation in database management systems (DBMS's). However, polyinstantiation is a specific solution to a problem faced by all secure systems, and the problem itself is not well characterized. The problem stems from the interference between subjects of different security compartments. The paper focuses on this problem which we have named Multi-party Update Conflict (MUC). We discuss and evaluate some solutions to the MUC problem, such as polyinstantiation and rigid classification. We describe a framework for a class of MUC solutions based on polyinstantiation, and enumerate several intermediate solutions between rigid classification and polyinstantiation. #ABSTRACT#461# Note: This paper discusses scheduling in Multi-Level Secure Databases. It is largely concerned with developing a theoretical framework for talking about scheduling and the properties of schedulers. It is fairly tightly tied in to the database environment. The paper is quite an enjoyable read, but ultimately I doubt that it contains much of use to people engaged in developing real schedulers. In particular the topic of timing channels, which is critically important in most scheduler designs is ignored. The paper defines three kinds of security property: BL-secure, DC- secure and CC-secure. BL-secure means secure against Bell and LaPadula; DC-secure means that there are no covert storage channels (DC stands for Data Conflict) and CC-secure means that there are no covert channels. Surprisingly the set of CC-secure systems is non- empty - but then this is a theoretical paper! The paper concentrates on DC-security. The meat of the paper is concerned with multi-version scheduling, so that the database stores more than one version of objects. A transaction consists of a sequence of actions. The scheduler regards actions as atomic events but may interleave actions from several transactions, thus creating potential interference between transactions. A transaction is, in the cases dealt with, carried out on behalf of one subject. Hence a transaction may be regarded as a single class event. The case of a principal subject making use of co-operating subjects at different clearances is mentioned but not addressed in detail. If a schedule can be expressed as a serial execution of its component transaction it is said to be serialisable. This is a desirable property because it separates contention within a security level from contention between security levels and so makes the analysis simpler. The paper explores classes of scheduler which do have such serialisability properties. An example is given of a scheduler which can be serialised in the multi-version case. The scheduler is shown to be DC-secure. The paper draws heavily on the work of earlier papers and uses a lot of database jargon. As a result it is quite an effort to get through to the fundamentals of the work. It also suffers from a lack of formality in places, which makes some of the definitions ambiguous, and so casts doubts on the results obtained. However it makes an interesting change from the run of the mill database papers. In this paper, we consider the application of multiversion schedulers in Multilevel Secure Database Management Systems (MLS/DBMSs). Transactions are vital for MLS/DBMSs because they provide transparency to concurrency and failure. Concurrent execution of transactions may lead to contention among subjects for access to data, which in MLS/DBMSs may lead to security problems. Multiversion schedulers reduce the contention for access to data by maintaining multiple versions. We describe the relation between schedules produced in MLS/DBMSs and those which are multiversion serializable. We also propose a secure multiversion scheduler. We show that the scheduling protocol outputs correct schedules and is free of covert channels due to contention for access to data, i.e. the scheduler is Data Conflict-Secure (DC-Secure). #ABSTRACT#462# This paper examines three techniques for evaluating the logical consistency of an object-oriented Database security model. The first technique consists of judging the model with respect to a set of general consistency properties for database security models. The second technique compares the SODA model against two other database security models. The third technique consists of defining a set of entities and mechanisms fundamental to the object-oriented model and considering the effect on them by the security model. Each of these techniques are applied to the Secure Object-oriented DAtabase (SODA) security model and are evaluated with respect to their applicability, difficulty and usefulness. Using the results of this analysis we characterize the consistency of the SODA security model. #ABSTRACT#463# Note: Abstract in TechGnosis, June 1989 (PO689-8). The rapid and sometimes poorly-planned introduction of data communications technology into the office environment can create opportunities for unauthorised access to both computers and data. Latest areas of high risk include the proliferation of data communications software, cellular telephones, local area networks, compact disk media, ISDN services, and satellite communications. Security weaknesses in office automation technology are highlighted and countermeasures, which minimise the risks while continuing to maintain efficient data communications, are recommended. #ABSTRACT#464# This paper presents a security policy for Separation Virtual Machine Monitors (SVMM's) and interprets Rushby's Separation Model for SVMM's. Applying the technique of Rushby yields a practical method for demonstrating that an implementation of an SVMM adheres to the abstract Isolation Axiom of the Separation Model, thus providing relatively strong assurance for a low level of effort. First we describe the relevant characteristics of SVMM's, and note the applicable formal modeling requirements. Next we present a summary of the SVMM Separation Model, a modification of the original model presented by Rushby. The Separation Model technique permits a proof of separability among the operating systems under control of the kernel of an SVMM. We supply an interpretation of the elements of the Separation Model using concepts from SVMM's. Finally, we relate this work to similar applications of the Separation Model. #ABSTRACT#465# Discretionary Access Controls (DAC) in object-oriented databases systems (ooDBS) are difficult to realize for several reasons: (1) the DAC concepts are more complex than usual due to the complexity of the data model and other factors; (2) access controls must often be applied to very small data granules if they shall be effective; (3) applications require mostly a very high performance of the ooDBS. This paper proposes a method for efficiently implementing access control lists (ACL's) in main memory ooDBS's. The main features of the method are: (1) ACL's are not stored directly, but via ACL numbers. (2) Each process has a cache which records results of evaluations of ACL's for this process and certain ACL numbers. #ABSTRACT#467# This paper is an introduction and summary of the (large) report R.A. Kemmerer 'Verification assessment study final report'. In the study four experts used four existing verification systems, Affirm, FDM, Gypsy and Enhanced HDM, on a set of test problems. #ABSTRACT#468# This paper presents an approach to analyzing encryption protocols using machine aided formal verification techniques. The desirable properties that a protocol is to preserve are expressed as state invariants and the theorems that need to be proved to guarantee that the cryptographic facility satisfies the invariants are automatically generated by the verification system. A formal specification of an example system is presented, and a weakness that was revealed by testing the formal specification is discussed. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 134 - 139 Richard Kemmerer illustrated an approach to analysing encryption protocols using the Ina Jo toolset. The emphasis of the paper is on the protocol rather than the encryption algorithm - the only assumption made is that decryption is the inverse of encryption. The paper emphasizes a role for testing in the analysis of formal specifications and illustrates this point with an example. For Kemmerer's original specification, this shows how a sequence of transformations can be exploited to gain a key in the clear. It is suggested that testing could be used to confirm a flaw in a protocol previously assumed to be secure. The points made in this paper seem sensible but they appear less convincing in the context of the simple example chosen, particularly since one of the flaws in the original specification was a previously known weakness of the protocol. Furthermore, there are some mistakes requiring correction in the formal specification and proofs. #ABSTRACT#469# The five volumes in this system cover pretty much the same ground as the paper by Cheheyl et al entitled 'Verifying Security' (ACM Computing Surveys 13(3), 1979). The areas covered in the volume reviewed here are: thoughts on the general topic of formal verification, including the alternatives, is formal verification the best approach, the need for formal semantics for the specification language; the relationship between security and verification, and the influence the former has had on the latter; a description of a state-of-the-art verification system; a discussion of what is needed to obtain production quality verification systems; comments on the next generation verification systems; a discussion of the verifiability of Ada; and finally, possible research directions. The remaining four volumes discuss the Gypsy, Affirm, FDM and HDM verification systems respectively. Each volume includes introductory remarks, a critique, a response to that critique by the system developers, and worked examples #ABSTRACT#470# Despite serious concerns raised by the proven ability of computer viruses to spread between individual systems and establish themselves as a persistent infection in the computer population, there have been very few efforts to analyze their propagation theoretically. The strong analogy between biological viruses and their computational counterparts has motivated us to adapt the techniques of mathematical epidemiology to the study of computer virus propagation. In order to allow for the most general patterns of program sharing, we extend a standard epidemiological model by placing it on a directed graph and use a combination of analysis and simulation to study its behavior. We determine the conditions under which epidemics are likely to occur, and in cases where they do, we explore the dynamics of the expected number of infected individuals as a function of time. We conclude that an imperfect defense against computer viruses can still be highly effective in preventing their widespread proliferation, provided that the infection rate does not exceed a well defined critical epidemic threshold. #ABSTRACT#471# In an effort to understand the current extent of the computer virus problem and predict its future course, we have conducted a statistical analysis of computer virus incidents in a large, stable sample population of PCs and developed new epidemiological models of computer virus spread. Only a small fraction of all known viruses have appeared in real incidents, partly because many viruses are below the theoretical epidemic thresh- old. The observed sub-exponential rate of viral spread can be explained by models of localized software e- change. A surprisingly small fraction of machines in ell-protected business environments are infected. This may be explained by a model in which, once a machine is found to be infected, neighbouring machines are checked for viruses. This "kill signal" idea could be implemented in networks to greatly reduce the threat of viral spread. A similar principle has been incorporated into a cost-effective anti-virus policy for organizations which works quite vell in practice. #ABSTRACT#472# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#473# VISTA is a high-level assembly language: its statements are essentially machine instructions embedded in an Algol 68-like syntax. It will be superseded eventually by NewSpeak for application programs, but in the interim it provides a reasonably friendly programming environment and a vehicle for writing a limited range of VIPER application software. VISTA is not a safe language, in the sense that NewSpeak will be, though it does limit the programmer to structures which are reasonably free of complications. 1T635. #ABSTRACT#474# Note: This paper discusses the ME2 (Military Message Embedded Executive) system and its underlying hardware TRUMMP (TRUsted Military Message Processor), which were developed from the MME (Military Message Experiment) sponsored by the US Navy and ARPA. This paper was presented by a colleague of the authors, who were unable to attend the conference. The presentation was, therefore, not as clear as it might otherwise have been. There does, however, appear to be an amount of substance in the paper, which may be worthy of further study. #ABSTRACT#473# The advent of the Trusted Network Interpretation (TNI) and the widespread availability of powerful microcomputers has resulted in the development of secure local area networking (LAN) products. Potentially, these products provide tremendous economic benefit by allowing multi-level secure operation of local area networks. This paper examines eight of the most popular secure LAN products from a technical perspective. The surveyed products include the Verdix Secure LAN, the Boeing Secure LAN, the Sun MLS OS, IBM/TIS's Secure Xenix, DEC's Ethernet Enhanced Security System, the Harris LAN/SX, the Ford Aerospace Multinet Gateway, and the Xerox Encryption Unit. Following the examination of these products, the paper provides subjective conclusions about the state of LAN security. #ABSTRACT#474# This paper describes a new mechanism for comparing selected program properties against a policy, or a set of rules, that states allowable program behavior. The motivation for this work is the increased need to control undesirable behaviors of programs, such as those inherent in Trojan horses and computer viruses. This mechanism, called an Automatic Policy Checker (APC), is currently implemented under SunOS. This paper will discuss the design and implementation of the APC and the application of the APC to the virus problem. Conclusions concerning anti-viral policy in light of the test results will also be presented. #ABSTRACT#475# This paper discusses a mechanism to aid users in the memorization of randomly generated nonsense passwords. The mechanism uses association and pictures and is based on techniques that have long been used as a means of memorizing information. The motivation for this work is the increased need to make passwords more difficult to guess and the necessity to keep them easy to remember. This mechanism makes an existing mechanism user-friendly, an area of computer security often ignored. #ABSTRACT#476# Note: This is a very matter-of-fact presentation of current (1988) international standards, mostly ISO, being considered by the US. Useful list of standards in the References list. #ABSTRACT#477# This is a special report presenting a view of the current state of the theory of distributed systems and pointing out the areas that need further work. It considers briefly loosely-coupled systems, but concentrates on tightly-coupled multiprocessor systems. #ABSTRACT#478# Note: PhD Thesis. #ABSTRACT#479# Auditing capability is one of the requirements for secure databases. A secure database management system, among other things, has to provide not only facilities for recording the history of all updates and queries against the database but high-level support for querying this history as well. In this paper, we present an audit model for object- oriented databases that satisfies both requirements. Our model offers several additional advantages: (1) it imposes a uniform logical structure upon both the current and the audit data; (2) it results in zero-information loss, ie. there is never any loss of historical or current information in this model; and (3) since it captures the entire database activity, a complete reconstruction of every action taken on the database is possible. We show how this third aspect can be exploited to provide high-level support for expressing audit and other database queries, and therefore, we make a complete audit trail methodology available. #ABSTRACT#480# Note: The Ulysses system is an interactive system which allows a user to model a system (h/w or s/w) and to make assertions about its security. The model takes the form of a collection of interlinked boxes, each of which may be internally composed of similar boxes. The boxes may be linked at specified points, known as ports, and, for each box, a section of code describes the ports and how they interact. Ports and links may be single-level, or multi-level. The code for each box may be a formal description of the actual intended code (using a language similar to ML), a nested specification involving other boxes and links, or a 'start-up' code, which overrides error conditions, allowing the model to be initially constructed without excessive error conditions arising at each stage. Once the model is constructed, the system performs flow analysis on the model, and either points out possible security violations. Part of Ulysses is a system which generates natural language from the formal specifications of each box. These take the form of 'The multiplexer is a component which accepts multi-level data through port A from component XYZ, and outputs single-level data through port B to component PQR, etc..' Some attempt is also made to describe the functionality of the specification. The examples of output were easily readable, and quite impressive. The Ulysses system is written in Lisp, and is currently Symbolics- based, although a Sun-based system is predicted. The Symbolics version was quoted to be 'deliverable soon'. The system was demonstated to the conference attendees, and the system appeared to perform well in a real-time environment, with a well-integrated user interface. The natural language generation from the specification was particularly impressive, and the system as a whole appeared to be a useful formal modelling tool. #ABSTRACT#481# The United States computer security community is one of the most influential forces in the international computer security arena. It has achieved this position by investing massive amounts of resources. Just the man/hours spent attending their annual national computer security conference often amounts to a yearly 35 man/years investment by the community. This massive investment has produced a socio-technical infra structure that is dynamic and vibrant but also very confusing for observers outside the United States. This confusion is often detrimental for the acceptance of US standards by the international computer security community. This paper attempts to shed light on the socio-technical infra structure of the United States computer security community by analysing the proceedings of the 12th United States National Computer Security Conference using the SBC socio-technical analysis methodology. The papers presented at the conference are classified using the SBC national-supranational analysis methodology. Once the papers are classified the SBC methodology is used to suggest trends and tendencies within the United States' computer security community socio-technical infra structure. #ABSTRACT#482# A security retrofit for UNIX that has had a degree of success. When you get to the end you discover that it has not all been done and there is no clear distinction between 'what is' and 'what might be' in the body of the paper. The main conclusion is that security can be added to an operating system provided that the base system is sufficiently simple and well structured. 1T7. #ABSTRACT#483# As an enhancement to the ISO's Open Systems Interconnection Model, the European Computer Manufacturers Association (ECMA) has developed a security reference model or framework for distributed systems. This framework is based on the concepts of security domains and security facilities and aims to provide a secure environment for both private application software and public communication services such as electronic mail. The different types of security domain within a distributed system are discussed and the scope of the ECMA framework outlined. A functional decomposition of security by the application of the ECMA framework results in a set of elements termed security facilities; these can be specified exactly and form building blocks for designing secure systems. #ABSTRACT#484# Working with formal specifications often involves an iterative cycle of development and change, either to correct errors discovered in a proof attempt, or to reflect changes in requirements. Making changes requires an understanding of the dependencies among terms in the specification. Boolean differences may be used to determine dependencies among functions in Boolean algebra. This paper introduces the notion of predicate differences in predicate calculus. The paper shows how predicate differences may be used to analyze the effect of changes to formal specifications; to investigate the conditions under which invalid assumptions will render a system non-secure; and in some cases may help to simplify re-verification of a modified formal specification. #ABSTRACT#485# Note: This paper describes a set of tools currently being used in the evaluation of electronic fund transfer software running on microprocessors, but which could also be used in other applications. These tools are written in C and designed for use on source code written in C. Among the tools described are ccalls, which produces a pair of matrices listing all routines called directly or indirectly by each routine in the system; by examining the latter, uncalled and unreachable routines may be identified. Other tools identify subsystems which are logically nested in their calling routines; include global variables in the analysis by treating them as functions; and identify all possible calling sequences. #ABSTRACT#486# This paper describes the application of formal specification and verification methods to two microprocessor-based cryptographic devices: a "smart token" system that controls access to a network of workstations, and a message authentication device implementing the ANSI X9.9 message authentication standard. Formal specification and verification were found to be practical, cost-effective tools for detecting potential security weaknesses, and helped to significantly strengthen the security of the access control system. #ABSTRACT#487# This paper proposes a mechanism for intrusion detection by audit data analysis. It is based on reconstructing high level activity from captured logs of low level activity, then analysing the high level activity for violations. This prevents bypassing of checks in the high level code on the main processor. An implementation monitoring a UNIX system uses a separate processor for analysis. This is a potentially interesting approach #ABSTRACT#488# Computer viruses pose an increasing threat to computer data integrity. They cause loss of valuable data and cost an enormous amount in wasted effort in restoration/duplication of lost and damaged data. Each month many more new viruses are reported. As the problem of viruses increases, we need tools to detect them and to eradicate them from our systems. This paper describes a virus detection tool: a generic virus scanner in C++ with no inherent limitations on the file systems, file types, or host architectures that can be scanned. The tool is completely general and is structured in such a way that it can easily be augmented to recognise viruses across different system platforms with varied file types. The implementation defines an abstract C++ class, VirInfo, which encapsulates virus features common to all viruses. Subclasses of this abstract class may be used to define viruses that infect different machines and operating systems. The generality of the mechanism allows it to be used for other forms of scanning as well. #ABSTRACT#489# The results of an experiment that shows that it is very simple to contaminate digital images with information that can later be extracted are presented. This contamination cannot be detected when then the image is displayed on a good quality graphics workstation. Based on these results, it is recommended that image downgrading based on visual display of the image to be downgraded not be performed if there is any threat of image contamination by Trojan horse programs. Potential Trojan horse programs may include untrusted image processing software. #ABSTRACT#490# A description of a proposed system that associates passphrases with users; the words of the phrase are drawn from a standard list, and the associated numbers may be entered instead. #ABSTRACT#491# We present an overview of a theory of modules and interfaces applicable to the specification and verification of systems with a layered architecture. At the heart of this theory is a module composition theorem. The theory is applied to the specification of a distributed system consisting of subjects and objects in different hosts (computers). Formal specifications of a user interface and a network interface are given. Access to objects, both local and remote, offered by the distributed system is proved to be multilevel secure. #ABSTRACT#492# Rapid advances in communication technology have accentuated the need for security in distributed processing systems. The broad interconnectivity provided by these technologies amplify both the capabilities of a computer network and the security risks. New developments in communication protocols promise to alleviate security problems by the application of standard security mechanisms. This paper examines significant work in the recent development of lower layer security protocols. Protocols for link, network, and transport layer security are examined and the architectural tradeoffs inherent in these mechanisms are contrasted. #ABSTRACT#493# The paper shows how a one-way function can be used to protect password information against unauthorised access, and extends this to prevent an eavesdropper being able to collect useful password information by listening to the communication between the terminal and the computer system. The user knows x, the system knows G(k,x), where G(i,x)=F(G(i-1,x)); when the user tries to log on, he is told i by the system and his terminal computes and sends G(k-i,x). The values of i given by the system should increase with time, and a new password is needed when k is reached. k must be small enough that G(k,x) can be computed in a reasonable time. 1T80. #ABSTRACT#494# This classic paper by Lampson introduces the Access Matrix model. The access matrix is a rectangular array with one row per subject and one column per object. The entry for a particular row and column reflects the operations that the corresponding subject can invoke on the corresponding object. The Access Matrix model specifies only that there are rules controlling access, but not what those rules are in detail. Because of this the Access Matrix model is more often used as a basis for more specific models than as a basis for an implementation. 1T46. #ABSTRACT#495# This collection of lectures deals with a number of important topics in distributed computing, each being presented by a single author. The lectures are independent of each other, which results in a certain amount of duplication, but do cover a great deal of ground. An extensive bibliography is included. Amongst the topics included are a number touching on aspects of reliable and secure systems such as naming, protection (which deals primarily with encryption but includes consideration of access control methods such as capabilities), atomic transactions and synchronization. #ABSTRACT#496# An interesting book by a dedicated, but caught, hacker, that describes the sort of techniques used by competent hackers to gain access to a computer system. The book also contains a survey of some security devices and their pitfalls, and gives quite a large amount of advice to those responsible for the security of computers. Recommended reading. #ABSTRACT#497# This surveys the then current (1983) state of various projects for secure computing; as well as summarising each of them, it also gives comparative tables and estimates of DoDCSC TCSEC ratings. There is an interesting section giving advice to developers of secure systems; this contains useful asides such as formal approaches are good not because they can be verified (they can't if there is much code) but because the discipline means the designers think about security and are more likely to notice loopholes. The summary gives the four main points of the advise: '(1) consider security requirements in conjunction with the user-visible behaviour of the system; (2) think about security throughout the design and implementation of the system; (3) use the best available software engineering technology; and (4) be sceptical; lots of 'modern' ideas don't work yet.' #ABSTRACT#498# This paper describes in detail many of the models that have been developed to describe particular requirements for handling data securely on computer systems. Most of these models have been based on the needs of military security, which combines heirarchical classifications and the 'need to know' requirement. #ABSTRACT#499# This two-page memo is by the person who was responsible for drawing up a security model for the military message experiment. In it he argues that the need to handle security levels is the direct result of policies mandated by government directive, whereas there is no such mandatory need for integrity levels. For this reason, and because he believes that integrity levels are not the right approach, he proposed to omit them from the model; the requirements for integrity would be covered by specific assertions as needed. #ABSTRACT#500# In addition to the work on security models for general purpose operating systems and the more general methods that can be applied to such systems, there has been some work on security models that are related to a particular application or class of applications. The most notable of these is the Military Message System model presented in this paper. In this model the emphasis is on the particular requirements of the application, especially those security features which are difficult to handle with a general multilevel security policy model. #ABSTRACT#501# Obstacles to achieving anomaly detection in real time include the large volume of data associated with user behavior and the nature of that data. This paper describes preliminary results from a research project which is developing a new approach to handling such data. The approach involves nonparametric statistical methods which permits considerable data compression and which supports pattern recognition techniques for identifying user behavior. This approach applies these methods to a combination of measurements of resource usage and structural information about the behavior of processes. Preliminary results indicate that both accuracy and real time response can be achieved using these methods. #ABSTRACT#502# This reference, often referred to as CR82, describes the four layers of services and protocols used on Cambridge Rings. These are for the R- service, P-service, V-service and the N-service which correspond to the ring component, packet, virtual circuit, and network independent services respectively. These services are not related to the OSI basic reference model in the document but, if they were the R-service would be in the physical layer, the P-service in the data link layer and the V- service and N-service in the network layer (the former possibly in a sub-network layer). The protocols for each service are otherwise known as: R-service: Mini-packet protocol; P-service: Basic block protocol (BBP); V-service: Byte stream protocol (BSP); and, N-service: Transport service byte stream protocol (TSBSP). The 'single shot protocol' (SSP) used for idem potent remote procedure calls is not documented. The standard also describes the concatenation and routing functions necessary at relays between two N-service implementations. An annex at the end gives a brief model for layer services, along the lines of that used in the OSI basic reference model. #ABSTRACT#503# Note: In this paper, the processes of granting clearances and accrediting trusted computer systems are compared, both informally (in Section I), and through mathematical models (analogies are brought out in Sections II and III). In Section IV, the combination of two TCBs is considered (the so-called ðcascading problemð). The example used involves two B2 TCBs, one accredited for a (TS,S) range and the other for a (S,C) range, and assumes they are connected by a single-level S channel. By the authorðs own admission, the analysis, and original modelling, use amateur mathematics and statistics. The conclusion, with certain qualifications, contradicts Appendix C of the TNI, which states that the assurance level associated with the combination of two TCBs is, in general, no higher than either given to the single TCBs. Under the assumptions that the Human Security Model (of Section II), the Computer Security Model (of Section III), and the ðYellow Booksð are all valid, and the two TCBs being combined are independent with respect to flaws and weaknesses, the conclusion is that the resistance to threat of a cascade of two B2 systems is roughly the same as that of a B3 system. It was pointed out during questions that, by a recursive argument, a number of D systems could be combined to be as resistant to threat as a B3 system! In general, the paper was met with indifference. #ABSTRACT#504# Note: Lee proposes the use of Integrity Categories and Partially Trusted Subjects together with the concepts of Secure systems at B1 (and above) to support the Clark and Wilson integrity model. An Integrity policy, consisting of a 'Simple Integrity Property' and an 'Integrity * - property' to be enforced by the system, is described together with a set of administrative procedures for setting up and running such systems. Each component of the Clark and Wilson model is addressed and expressed in terms of the described procedures, integrity properties and TCSEC features. A number of miscellaneous topics are addressed showing that the approach taken by Lee is at an early stage and needs further exploration. The relationship between this proposal and accepted computer security techniques should make this paper of interest to CESG if it becomes necessary to consider how integrity related functions (eg roles) can be included in the upcoming generation of Secure Systems. It should be noted that Integrity policies and implementation techniques are clearly at an early stage in development, compared to their security counter parts, and further work is needed to support their useful application. Government research, development, and standardization efforts in computer security have been repeatedly criticized as not being applicable to the commercial world. In particular, they have been criticised as not being able to support the kinds of security policies, such as separation of duties and well-formed transactions, used by the financial and other communities to control unauthorized changes to or falsification of information. This paper demonstrates how two natural extensions - integrity categories and partially trusted subjects - of the principles of current DoD computer security standards could be used to implement such commercial security policies in a way that exploits the fundamental strengths of existing or future trusted systems. #ABSTRACT#505# Note: The paper would be more correctly entitled ðA Formal Model for the GEMSOS Discretionary Access Controlð. Gemini is engaged in the development of a UNIX-compatible interface to be supported by an underlying TCB evaluated at A1. A distinguishing feature of the UNIX operating system is the setuid mechanism. The setuid mechanism allows processes to gain permissions which they did not originally have. This poses a possible threat to any DAC policy. In his presentation Steven J Padilla described the difference between UNIX and the Bell and LaPadula model in the way that subjects gain access to objects as: Suppose Object Island is connected to Subject Land by a bridge. On the bridge is a customs officer (Mr Permission) who allows subjects access to Object Island if they have the right permission. In Bell and LaPadula the subjects arrive individually. Each is checked to see if he has the right permission. In UNIX the subjects arrive by the busload, but only the driver is checked. The GEMSOS model seeks to retain as much of the setuid mechanism as possible, but still maintain a DAC policy. This is achieved by restricting the semantics of the setuid mechanism. These restrictions take the form of three modelling and four policy requirements. The modelling requirements are: „ A process will be represented by a different subject after a change in DAC identifier. „ Each object will have an associated DAC identifier. „ A new access mode ðcontrolð. The policy requirements are: „ A process can only assume the DAC identifier that has been associated with an object. „ A process can assume the DAC identifier associated with an object if the process has execute access to that object. „ The DAC identifier of an object can only be changed to that of a calling process if the identifiers have more than one aspect (eg. user and group). „ The DAC identifier of an object can only change to that of a calling process if the process has control access to that object. The paper claims that the GEMSOS model can be derived from the principles of Bell and LaPadula. It then goes on to compare the GEMSOS model with the Bell and LaPadula model. This comparison is done under three headings; Elements, Properties, and Rules. Nothing is said about the Rules as these are application specific. Under the Elements section the notions read-class and write-class are introduced. In the GEMSOS model the access of subjects to objects is more limited than in the Bell and LaPadula model. This is because the Bell and LaPadula model effectively has the write-class as system low. Under the Properties section it is pointed out that in the GEMSOS model the removal of permission does not result in immediate revocation of access. This is not the case in the Bell and LaPadula model, although it is claimed that the two are equivalent in terms of information flow. The paper finishes with a justification for having a separate DAC model (as opposed to a combined DAC and MAC model), and a formal presentation of the model in the Ina Jo language. This model formalises the three modelling and four policy requirements listed above. #ABSTRACT#506# This paper describes the advantages and disadvantages of using the Front End approach to database security. It argues that one such approach, known as an "Integrity Lock" is unnecessarily complicated and shows that adherence to the SQL standard causes a performance penalty. #ABSTRACT#507# It is proposed that all database security controls, except those which provide information flow security, can be built using a suitable trigger mechanism. The implementation of an example application, which has a variety of requirements for confidentiality, integrity and accountability, is shown to illustrate the technique. The trigger mechanism is to be implemented using query modification as part of the SWORD secure DBMS project. #ABSTRACT#508# This Datapro report is based on a paper by the NBS presented at the 1986 DOD/NBS NCSC. #ABSTRACT#509# In Brewer and Nash's Chinese Wall security policy model, there is a very strong implicit assumption that the "conflict of interest" is an equivalence relation. It is called the BN-axiom. Such axiom is valid only for some very special circumstances. By modifying their formulation, a modified Brewer and Nash model without BN-axiom is defined. Such model turns out to be rather "conservative" in the sense that the Chinese Walls are built within Chinese territory; it is not really a Chinese Wall model. Next, a new formal model is introduced in which Chinese Walls are built right on the boundary of China - an aggressive model for Chinese Wall security policy. #ABSTRACT#510# Note: Introduction: Aggregation and inference problems have been investigated by various authors. In our recent works, we have proposed a solution to settle the aggregation problems in design phase; solutions during the query processing time will be reported in the near future. In our recent works, we have investigated not only the case of one aggregate (all classical works belong to this case), but also the case which consists of "empires" of aggregates. For the case of one single aggregate, our solution has almost the same effect as Lunt's solution. Both solutions need SSO (System Security Officer) to downgrade or release the internal data of an aggregate. Without some practical guidelines or references for SSO, the applications for either solution will be limited. However, the nature of such guidelines or policies may very well be application dependent; hence there might be no common guidelines or policy across the applications. This paper proposes a probabilistic type of measure theory which estimates the amount of security relevant information of every subset of a given aggregate. This probabilistic measure theory provides each application a means or mechanism to furnish the system a numerical measure to assist the SSO for making decisions on releasing or downgrading the internal data of the aggregate. Combining this measurement with our previous results, a scenario for solving the aggregation problems during the design phase is proposed. In developing this work, two guiding principles are applied: Minimum Aggregation Principle (MAP) and the Maximum Protection Principle (MPP). MAP keeps both the number of elements in an aggregation and the number of aggregates to a minimum, while MPP keeps the unnecessary risks to a minimum. #ABSTRACT#511# Note: This paper describes a system which attempts to find the dominant causes of a program proof failure in the HDM system. This is done by logging and categorizing each error as it occurs, and, when more than a specified number of categories have been identified, these are merged into larger categories. In this way, groups of 'symptoms' are collected, such that each group corresponds to one proof 'bug'. When originally presented, an example was given that made the principle of the system somewhat more obvious. Unfortunately, this example was omitted from the papaer in the Proceedings. #ABSTRACT#512# Discusses issues related to authentication in a distributed computing environment, and descrives authentication approaches employed in DEC's Distributed Systems Security Architecture (DSSA). Node, User and proces granularity authentication concerns are considered. Authentication is based on a global hierarchic naming structure and public-key cryptography. Directory-resident certificates associating entities with long-term keys are used in conjunction with dynamically signed certificates which represent transient bindings between entities. Distributed system elements can be mutually suspicious. At the node level, special topics considered include the relationship between authentication and secure loading and the relationship between authentication and rule-based policy support. At the user level, architectural requirements are identified and authentication protocol options based on smart cards and on user-entered passwords are described. #ABSTRACT#513# Note: This paper discusses various aspects of Authentication within the DSSA structure. Some of the ground of the previous paper is re-visited, but at a somewhat more abstract level. Once again the approach is heavily influenced by the availability of public key cryptography. Authentication is discussed at three levels of granularity. Firstly at that of interacting computer systems on a network, secondly at that of human users and finally at that of application processes. The architecture is claimed to work between mutually suspicious security authorities as well as within a single authority. The basic technique is that described in the previous paper where a certificate carries a public key and a digital signature. Certificates may be long term (identity certificates) or short term (dynamic binding certificates). The User Authentication Architecture is claimed to be compatible with various levels of user authentication device ranging from smart cards offering RSA capabilities down to simple passwords. Techniques are described for using the RSA smart card, which is the preferred method within DSSA and two approaches using passwords are also given. The paper provides a discussion overview of the approach adopted to authentications in DSSA but does not provide much in the way of technical detail. #ABSTRACT#514# An update on the status of work on program confinement and covert channels. Although it is now fairy old it still contains some important points not seen in later papers. Required reading for anyone working on confinement or studying covert channels and Trojan horses. 1T48. #ABSTRACT#515# The first section of this paper introduces the basic notion and derivation of the lattice model. It also introduces, for purposes of comparison, the results of a previous attempt to apply the lattice model in a commercial environment. The second section examines commercial requirements for information security and derives an alternate application of the lattice model more suited to these requirements. The final section introduces a second component of the lattice model (the integrity model) and revisits the commercial application to show an alternate formulation for achieving security. The paper's main conclusions are that the lattice model may in fact be applicable to commercial data processing, but that such application will require ways of looking at security requirements different from those prevalent in the national security community. The joint involvement of people experienced in commercial applications and of people who understand the lattice security model will probably provide the most productive course towards the development of successful commercial applications of the lattice model. Referenced by the TNI (Red Book). #ABSTRACT#516# Authentication methods are classified by IS (such as measuring a physical characteristic), DOES (such as measuring how an action is performed), HAS (such as possession of a key, card, etc), KNOWS (can quote a password, say), and RECOGNISE (can identify a pattern). The various methods in use or proposed are then described and discussed. #ABSTRACT#517# The DLCN is envisaged as a powerful, unified distributed computing system which interconnects heterogeneous midi/mini/micro- computers etc. This paper gives an overview of the design requirements and implementation techniques for DLCNs, message protocol and network operating system. It is a hypothetical system to be used to investigate fundamental questions of distributed computing. Its description varies between very detailed (the message protocol) to completely general. Probably reflecting the achievements current at the time of reporting. This paper is an interesting example of the design of a distributed system, but has no specific computer security implications. #ABSTRACT#518# Note: Published as Vol 23 No 5 of OSR. #ABSTRACT#519# Within the Department of Defense developers have been designing and implementing a prototype multilevel secure local area network (MLS LAN). Researchers at MITRE have been cooperating in this development by doing the security modeling. The MLS LAN has special dynamic features, such as the ability to add new security levels during normal operations and to modify label translation schemas, which distinguish it from other secure LANs. These features enhance the functionality of the LAN without compromising its security. This paper highlights the principal features of the MLS LAN and discusses some of the design, implementation and modeling issues. #ABSTRACT#520# This paper presents an algorithm for key distribution across connected networks each with their own ACS. It makes a number of assumptions, such as: encryption is at the session layer, using the same algorithm in each network; there is to be minimal or no modification to existing key distribution protocols at nodes (for use within a network); and, the ACS/gateway software can be readily adapted. The usefulness of the work depends on the validity of these assumptions in a particular environment. 1T453. #ABSTRACT#521# An efficient design of the security architecture for a computer network requires the integration of security implementation considerations with a formal security model describing the security policy in the network. The distributed nature of the network, however, offers complexities in the development of appropriate models. In this paper, a new model which precisely describes the mechanism that enforces the security policy and requirements for a multilevel secure network is described. This mechanism attempts to ensure secure flow of information between entities assigned to different security classes in different computer systems connected to the network. The mechanism also controls the access to the network devices by the subjects (users and processes executed on behalf of the users) with different security clearances. The model integrates the notions of nondiscretionary access control and information flow control to provide a trusted network base (TNB) that imposes appropriate restrictions on the flow of information among the various devices. Utilizing simple set theoretic concepts, a procedure is given to verify the security of a network that implements the present model. #ABSTRACT#522# The Bell-LaPadula model for secure systems is stated in mathematical terms. It is then applied to Secure Xenix and shown to be correctly supported. This is a fairly long-winded paper with some Xenix detail. It could be useful if applying the model to other systems. #ABSTRACT#523# Note: The aim of the paper was to define more clearly the kinds of inference and aggregation problems. Having done so she argues that many of these so-called problems are not really problems and can be tackled by sensible design of the database. That is, no mechanism beyond MAC is required. The gist of this is neatly illustrated by the following example. Suppose that employee names are unclassified and salaries are unclassified. However, the associations of an employee with his salary is considered classified. This is neatly handled by setting up a database with: (i)ð a list of employees against employee number; (ii)ð a list of salaries against salary number; (iii) ða list of employee numbers against salary numbers. (i) and (ii) are unclassified whilst (iii) is classified. The spirit of the presentation was that inference and aggregation problems have probably been given undue emphasis. They can generally be handled by appropriate design of database and assignment of classification. This, after all, is essentially how it has been done in the paper world. On the other hand, tools can probably be supplied to assist in this design process. Tools, for example, to flag potential inferences. It was pointed out that a number of problems remain to be understood better. These include the effect of external information, statistical attacks and dynamic information (derived from observing changes in the database). #ABSTRACT#524# Note: Distributed as Tutorial Notes at 4th Aerospace Computer Security Applications Conference. #ABSTRACT#525# Note: This is just what it says: a good (though a bit long) survey of recent work in the field. It seems to come to the conclusion (not explicitly) that this approach has yet to come to fruition. #ABSTRACT#526# Note: The IDES project is developing a prototype Intrusion-Detection Expert System, to test the theory that misbehaviour by a user can be automatically detected by looking for variances from their normal behaviour patterns. The prototype is implemented as a stand-alone system, collecting and collating information provided by the systems being monitored; currently the actions being analysed include login, logout, running a program, invoking system calls and using the network. It maintains various measures of the current behaviour of each active user, and continually compares these against historical records. Deviations by more than a preconfigured amount cause alarms. Over a period of time the historical records are altered to reflect the current pattern of working, so allowing a gradual drift in a user's habits to happen without causing alarms. The system has been used to monitor a DEC machine running a locally- modified version of TOPS-20 capable of supporting up to 128 users; the operating system has been modified to gather and preprocess audit data, transform it to IDES format and transmit it in an encrypted form, without noticeable degradation of its performance. IDES has detected various simulated intrusions, usually within a minute of the event occurring, though it has not yet been tried on the audit trails of systems that are known to have been penetrated. Work is underway to determine other measures that could be used to detect intrusions of various types, including clandestine use and also misuse of their privileges by authorised users. Describes the design and implementation of a prototype intrusion- detection expert system (IDES) developed at SRI International. IDES is based on the concept that an intrusion manifests itself as a departure from expected behaviour for a user. The prototype monitors users on a remote system using audit records which characterize their activities. It adaptively learns normal behaviour of each user and detects and reports anomalous user behaviour. #ABSTRACT#527# Note: This was the second of two papers in the proceedings from SRI and Gemini on the Seaview multilevel secure relational database project. This paper describes a design for Seaview which can be implemented 'in the near term'. In essence the proposal is to use a commercially available off-the-shelf security kernel (GEM-SOS) and a commercially available relational database (Oracle). Oracle will need some modification. Additional specific code for Seaview will need to be written. There is an interesting discussion of TCB subsetting, leading to four classes of trust, which could map onto GEM-SOS protection rings: „ verified kernel for mandatory security „ enforcement of non-mandatory policy „ still-less-trusted: for example, database manager „ user-written applications. In summary, the two Seaview papers represent a very fine example of what US technology can achieve. There is a drawing together of work in two different fields, security and relational database, into an integrated whole, with a considerable amount of original work to make the whole. There are engineering as well as theoretical problems for which a solution is needed and is available. There is a practical emphasis and a clear distinction between short-term and long-term goals. The SeaView formal security policy model admits a range of designs for a multilevel secure relational database system. The requirement for a near-term implementation suggests that the design should utilize existing technology to the extent possible. Thus the design uses an existing database management system ported to an existing TCB environment. A preprocessor translates key constructs of the SeaView multilevel relational data model used by the commercial database system. The underlying reference monitor enforces mandatory and basic discretionary controls with A1 assurance. Discretionary controls on relations and views as well as the enforcement of data consisency are provided by the commercial database system. The key technology introduced in this paper is that by combining single level data into a multilevel view, a commercial database system can be used and data can be classified at the relation level to implement the SeaView model, with element-level classification. #ABSTRACT#528# This paper describes a real-time Intrusion Detection Expert System (IDES) that observes user behavior on a monitored computer system and adaptively learns what is normal for individual users, groups, remote hosts, and the overall system behavior. Observed behavior is flagged as a potential intrusion if it deviates significantly from the expected behavior or if it triggers a rule in the expert system rule base. #ABSTRACT#529# Note: Revised version of IEEE Symposium paper. A multilevel database is intended to provide the security needed for database systems that contain data at a variety of classifications and serve a set of users having different clearances. This paper describes a formal security model for such a system. The model is formulated in two layers, one corresponding to a reference monitor that enforces mandatory security, and the second an extension of the standard relational model, defining multilevel relations and formalising policies for labeling new and derived data, data consistency and discretionary security. The model also defines application-independent properties for entity integrity, referential integrity and polyinstantiation integrity. #ABSTRACT#530# A security model for the SNet multilevel secure distributed system, based on a behavioural semantics for operator nets and expressed in Lucid, is described. This model subsumes a previously published model of the network within SNet and includes authorized downgrading as well as the security policies enforced by trusted hosts connected to the network. The previous model described in this paper provides a more general abstract model than is provided by those seven constraints. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 150 - 160 This paper describes a security model for a multilevel secure system (SNet), expressed using operator nets and Lucid. The objectives of the SNet project is to develop a multilevel secure system with a minimum of trusted mechanism. The paper describes a system similar to the DSS proposed by Rushby and Randell, in which trusted network interface units (called ladels) mediate access over the network to untrusted hosts. The SNet enforces a security policy which allows only upward flow of information with respect to the lattice structure of security labels, unless through the intervention of a trusted downgrader. An operator net is a graph consisting of nodes and directed arcs. The nodes represent the active components of SNet (e.g hosts), and arcs represent the communication channels between nodes. Lucid is a functional programming language used to implement operator networks. Each node in an operator net is defined as a function in Lucid which maps the history of communications in the input arcs to a history of communications on the output arcs. The paper uses the combined operator net/Lucid formalism to give detailed specifications of the SNet at both the security model and component model levels. Consistency between these levels is also discussed. #ABSTRACT#531# Note: Graduate Texts in Mathematics No 3. #ABSTRACT#532# The concurrency control algorithms used for standard database systems can conflict with the security policies of multilevel secure database systems. This paper describes two new concurrency control algorithms that are compatible with common security policies. They are based on the multiversion timestamp ordering technique, and are implemented with single-level subjects. The use of only single-level subjects cannot introduce any additional threat of compromise of mandatory security; our analysis will focus on correctness. One of these algorithms has been implemented for Trusted ORACLE. #ABSTRACT#533# A potential problem in all multilevel networks is cascading. This problem can be eliminated in static networks by applying the nesting condition. The nature of dynamic networks prevents the use of the nesting condition. This paper introduces the concept of a Unidirectional Nesting Condition and provides proofs that show the Unidirectional Nesting Condition sufficient and sometimes necessary to prevent cascading in dynamic networks. #ABSTRACT#534# The paper presents a list of considerations for applying a commercial off-the-shelf disk encryptor to an environment where hostile overrun is a significant threat. The considerations include: how the encryption device is configured and interfaced to the workstation, host, or server; encryption key management including key entry, changeover, and quick destruct; and long term off-line storage. #ABSTRACT#535# The National Computer Security Center has issued guidance for Trusted Computer Networks called the Trusted Network Interpretation (TNI) of the Trusted Computer System Evaluation Criteria (TCSEC). The TNI provides requirements for trusted computer networks that extend the guidance provided for traditional stand-alone computer systems by the TCSEC. It is expected that this Department of Defense (DOD) technical security guidance will be used as the basis for certification of DoD network system acquisitions. This paper presents three major steps illustrating an application of the TNI. The steps are: 1) formulating a TNI view; 2) determining the appropriate TNI security requirements that will apply; and 3) formulation of a network security architecture based on the allocation of the determined security requirements. #ABSTRACT#536# Proposes a rigorous mathematical definition of the concept of a variable being read by a process. This is shown to correspond to the normal intuitive meaning, and then is shown to be theoretically decidable. 1T522. #ABSTRACT#537# This paper presents the initial results of a DARPA-funded (The work reported in this paper was supported by DARPA Order 6414 under contract MDA 972-89-C0029 to TRW Systems Division) research effort to define a development paradigm for high-performance trusted systems in Ada. The paradigm is aimed at improving the construction process and the future products of Ada systems that require both broad trust and high performance. The need for a Process Model and the notions of trust and assurance are reviewed. The foundation for the Process Model and its elements are presented. The Process Model is contrasted with traditional development approaches. The combination of a risk driven approach with the integration of trust and performance engineering into a unified whole appears to offer substantial advantages to system builders. #ABSTRACT#538# This paper describes the reasoning behind various acts and ammendments (past, present, future and rejected) that affect the requirements for privacy in computer systems. It does not concern itself with multilevel security. #ABSTRACT#539# This paper looks at a suggested technique for inference control in statistical databases, that of perturbing the values by adding noise. The motivation is to ensure individual values cannot be determined; the hope is that if the noise has a mean of zero, the operation in unbiassed. The paper claims this is not true, as we are always interested in conditional means. An assumption is made that the noise is added to the figures in the database. Possible solutions to avoid the bias are to add the noise to some fields only, which requires the searches to be restricted, or to compensate for the bias, which is complex for multivariate samples. The latter approach is under investigation. #ABSTRACT#540# In the Open Systems Interconnection (OSI) communication framework, standards are being proposed for cryptographic-based security protocols that will provide security services to the user. Many of these security protocols provide almost identical security services and are being pursued in groups that include ANSI, IEEE, IETF, and NATO. This paper examines two of the current security protocols defined for the Network Layer of the OSI communications stack that are being proposed for use by Department of Defense and commercial networks and the issue of interoperability between these two protocols. #ABSTRACT#541# This note presents a precise summary and comparison of two environmental guidelines for secure systems: that developed by the National Computer Security Center (ie. the "yellow books") and a competing methodology proposed by Landwehr and Lubbes of the US Navy. Both methodologies are described and applied to a hypothetical example along with a discussion of the strengths and weaknesses of each. #ABSTRACT#542# Note: This paper examines the extended Bell-LaPadula model (as defined by Bell in 1986), and concludes that it is inconsistent, and should be further extended to become consistent. Bell's model associates with every subject a maximum viewing clearance and a minimum writing clearance. The rationale for this is that it minimises the number of subjects which need to be trusted to perform write-down operations. One example of the quoted inconsistency is that, in Bell's system, a subject may create a child which may read objects which the parent may not, and may communicate this information back to the parent. It is argued that the restriction which prevents direct access by the parent is, therefore, pointless. The paper also describes the implementation of the scheme in TMach. This appeared to be an interesting paper which would be worthy of studying in detail. #ABSTRACT#543# In recent years it has been recognized that the protection of classified and sensitive information in a distributed, automated processing environment requires a total "information security" (INFOSEC) solution, combining both communications and computer security technologies into an integrated security solution. While the need for INFOSEC solutions is clearly recognized, the commercial availability of true INFOSEC products is extremely limited or non-existent. This paper discusses the evaluation issues involved in an effort to take evaluated COMSEC technology and evaluated trusted system technology, and integrate them into an evaluatable INFOSEC product. #ABSTRACT#544# Note: This paper is mainly concerned with the interfacing of a risk management tool, which was still at a fairly early stage of development. It uses an 'expert system' type knowledge base and hierarchical decomposition of problems to reduce the difficulty of describing a system to the tool. The paper does not seem to introduce any significantly new ideas. #ABSTRACT#545# This paper deals with the issue of preserving and promoting integrity within computer and automated information systems. It is intended to serve as the starting point for defining those expectations and standardizing integrity properties of systems. The paper discusses the difficulty of developing a single definition of the term integrity as it applies to data and systems. Integrity has multiple definitions in the dictionary and the application of those definitions to data and systems using a single attribute within the expectation set has led to definitions that could not achieve consensus. Concluding that a single definition is not needed to advance our understanding, the paper develops a more appropriate operational definition, or framework, that encompasses various views of the issue. This framework includes the two distinct, yet interdependent, contexts for integrity: data and systems. The Framework reinterprets, within these two contexts, a general integrity protection goal to derive three specific integrity goals. The framework also interprets the integrity properties and relationships of active and passive entities in a system using the conceptual constraints of "adherence to a code of behaviour," "wholeness,"and"risk reduction." The paper concludes that it is possible to begin to standardize integrity properties. We acknowledge that gaps in understanding exist, but recommend that further studies be undertaken. We conclude that such studies can be accomplished concurrently with standardization and that both efforts could be mutually supportive. #ABSTRACT#546# All computer systems are vulnerable to abuse and penetration by both legitimate users who abuse their authority and individuals who are not authorized to use the computer system. Many systems are under development to aid in the detection of these abuses. The capabilities of these "intrusion detection systems" (IDS) are varied ranging from tools that provide for the meaningful reduction of audit data to tools that provide in-depth analysis of user and system behavior. The authors have performed a survey of the state-of-the-art in intrusion detection systems (IDS). This paper presents a summary of this survey. #ABSTRACT#547# Note: This paper starts by describing classification systems in the DoD and intelligence areas, which cannot be implemented using straightforward MAC and DAC based on individual or group privileges. The paper proposes two systems of access control which solve these problems, Owner Retained Access Control (ORAC) and an attribute based access control system. The paper discusses the problems of implementing these policies. The ORAC system is based round the labelling of objects in the system, copies of these objects then inherit the access constraints of the original object. This inheritance is dynamic, in the sense that modification of the constraints on the original causes modification of the constraints on all the copies. The access controls on the copy can also be added to, to increase the access constraints on the object. However, the original access constraints cannot be weakened except by the owner of the original object. The attribute based access control system proposed is based round the labelling of objects, when a subject then attempts to access an object the attributes of the subject are checked against the objects list of attributes which describe the characteristics of subjects which are allowed to access that object. For example the subject may have to be British and not have blue eyes. Although both ORAC and the attributed based system provide a fine granularity of access control there are high penalties to be paid for in terms of computational overheads. As they are implemented through the use of logic based labels, which can be fairly complex. The other major disadvantage of the system is that the constraints on access to objects steadily increases as the objects are copied or accessed. Designers of trusted systems have thus far concentrated almost exclusively on providing access controls according to the mandatory discretionary access control paradigm, with mandatory access control based on a lattice of sensitivity labels and discretionary access control based on individual and group access privileges. This paper discusses some examples of DoD/intelligence data protection requirements that cannot be handled through traditional MAC or DAC and proposes two new forms of access controls to respond to these problems. First, a user attribute-based access control for enforcement of dissemination controls is introduced. Second, a type of access control know as Owner-Retained Access Control is described, to provide a privilege-based form of access control that, unlike DAC, prevents access to data being extended to others without the owner's concurrence. For both types of controls, the access control rules to be enforced and the implications of providing automated enforcement of these controls are discussed. Finally, a comparison of the two forms of control is made, and an informal model is presented that provides a common framework for representing both. In conclusion, the benefits and drawbacks of this approach are discussed, and some areas for future work are identified. #ABSTRACT#548# Note: Revised version of IEEE Symposium paper. In this paper, the author describes a security property for trusted multilevel systems, restrictiveness, which restricts the inferences a user can make about sensitive information. This property is a hookup property, or composable, meaning that a collection of secure restrictive systems when hooked together form a secure restrictive composite system. The author argues that the inference control and composablity of restrictiveness make it an attractive choice for a security policy on trusted systems and processes. #ABSTRACT#549# Note: This is due to be published by the USAF Systems Command at Rome Air Development Center. #ABSTRACT#550# Note: This introduces the problems of nondeterminisim and interruptability. Most McCullough examples in this and the earlier paper depend on the type of sequence described in the first two paragraphs of section 5 p184. It attempts to deal with the problem of systems which are either non-deterministic or interruptible, either of which features cause problems with earlier theories; input buffers, since they cannot be made infinite, may either 'block' or lose information. If input buffers are blocked, covert channels may be introduced - the author produces a neat subsystem which violates MLS in gross fashion by using the blocking of input buffers. If they lose information when full, then nondeterminism is introduced; Nondeterminism can also be introduced by using parallel processing. There is thus a need for a generalisation of Goguen and Meseguer to incorporate the idea of non-determinism. Finally the author proposes a further property, which he calls 'restrictiveness'. He goes on to produce a state-machine characterisation of restrictiveness and to compare its good and bad points with those of Goguen and Meseguer noninterference, generalised noninterference and Sutherland deducibility. The Problem of composability of multi-level security properties is discussed, particularly the noninterference property and some of its generalizations. An attempt is made to show through examples that some of these security properties do not compose - it is possible to connect two systems, both of which are judged to be secure. Although the examples are 'cooked up' to make a point, there is nothing especially tricky done; McCullough ensures that outputs from one system become inputs to the other machine at the same security level, and uses a standard notion of parallel composition of systems. #ABSTRACT#551# In this paper we give a brief description of several formalisms for computer security, and discuss some of the problems in their interpretation an application. We define the property of 'hook-up security', which can be shown to imply that a collection of hook-up secure systems can be hooked up to form a secure complex system. We believe this result addresses some of the problems with other definitions of security, and will be valuable in the design of large secure systems from simpler secure components. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 161 - 166 This is an interesting and significant paper. Its subject is a formulation of a security property which may hold for an isolated system and which may also hold for the connection of such systems in a simple way. (The simple form of connection is to permit the exchange of securely-labelled messages by identifying outputs of one system with inputs of another, separately for each security class). It turns out that in general it is not necessarily the case that 'secure systems securely connected' are as a whole secure, given an arbitrary notion of security, or even a well-established notion such as non- interference. Clearly this is bad news from the point of view that designers want properties of complex systems to be decomposable into properties of simple components. A property is defined, called 'hookup security'; this is a strengthened form of non-interference. The strengthening is a condition on the relative order in which certain input and output events may occur. It must be said that the style of this paper is far from clear. There are some evident textual errors, there is a crucial obscurity in the main example which motivates this treatment, and if the definition given of non-interference has been correctly understood, then it is difficult to accept. The result is that there is some difficulty in being sure the author's intentions have been understood. However, this is a stimulating paper: its ideas merit more study, and will certainly help to sharpen notions of security. #ABSTRACT#552# Note: Introduction (part of): At speech to the 13th National Computer Security Conference on 3 October 1990, Michelle VanCleave, Assistant Director for National Security Affairs, Executive Office of the President stated, "We need a comprehensive model for understanding the threat to our automated information systems." I believe I have developed that model. This model not only addresses the threat, it functions as an assessment, systems development, and evaluation tool. The model is unique in that it stands independent of technology. Its application is universal, and is not constrained by organisational differences. As with all well defined fundamental concepts, it is unnecessary to alter the premise even as technology and human understanding evolve. #ABSTRACT#553# This paper addresses composability properties of component systems. By means of analysis of external relations among components, security problems associated with composition of the components are investigated. To solve these problems, two security models are presented. By comparing these two models, important properties of secure composition of component systems are identified. #ABSTRACT#554# This paper presents some initial experiences in NRL's application system certification technology project. The project goal is to develop an approach to certifying US Navy application systems that must be trusted. We are conducting our research by participating in the certification of two NATO command and control systems targeted at the B3 class of the Trusted Computer System Evaluation Criteria. An important initial finding of this project is a working definition of the role that an informal and descriptive top-level specification plays in development of trusted application systems. Other initial experiences include the possibility of using the descriptive top-level specification as a preliminary specification and the identification of some easily corrected shortcomings of natural language descriptions. The paper is divided into two parts. The first part discusses the role of the descriptive top-level specification and the second part relates three initial experiences with descriptive top-level specifications. #ABSTRACT#555# The replicated architecture for multilevel secure database systems provides security by replicating data into separate untrusted single- level database systems. To be successful, a system using the replicated architecture must have a concurrency and replica control algorithm that does not introduce any covert channels. Jajodia and Kogan have developed one such algorithm that uses update projections and a write- all replica control algorithm. Here we describe an alternative algorithm. The new algorithm uses replicated transactions and a set of queues organized according to security class. A new definition of correctness is required for this approach, so we present one and use it to show that our algorithm is correct. The existence of this new algorithm increases the viability of the replicated architecture as an alternative to kernelized approaches. #ABSTRACT#556# Information flow analysis is required for A1 certification, so a flow analysis tool has been developed to assist in this,the paper contains a brief overview of this. A new Gypsy abstraction is introduced, which defines an abstract type called information and the functions which operate on the type. The tool uses this abstraction with the results of the Gypsy optimiser (which contains an analysis tool to detect 'ghost' unused variables) to detect all potential flows. The tool is normally used by first identifying the TCB and its 'interface set' (the externally visible components of the TCB), then analysing the TCB flows, and then producing information flow analogues for the TCB set. Information policy specifications and verification conditions can then be developed for the TCB interface set, and the VCs proved. There are three main problems with this approach: most contrary flows revealed are due to potential exceptions that will not occur in practice, many programs will be acceptable despite certain contrary flows, and the tool does not at the moment let the user discover the path of information flow. Furrther work is needed to maintain path information, reduce the need for a skilled user, and to integrate flow analysis with proofs about exceptions and blockages. #ABSTRACT#557# The Verdix Corporation is producing a secure multilevel LAN, which has been accepted for developmental evaluation by NCSC. Hosts are connected to the network via a Network Security Device, using shared memory for data transfer between the NSD and the host. Mediation is performed by both ends whenever a message is sent, with protocols requiring no host-host acknowledgement. A Network Security Center is responsible for updating tables in the NSDs defining the security policy, and also issues encryption and decryption keys for each 'association' (NSD to NSD path). The security policy defines only the interaction between the Trusted Network Base (TNB) and the outside world. The model is a simplified version of the Bell-LaPadula model; objects are datagrams, subjects are hosts, and the security classes are drawn from a lattice. Unlike Bell-LaPadula, objects are very temporary, and subjects are assumed to have access to information up to and including their clearance. There is a single operation, communication (Si,Oijx,Sj), which is permitted if: the class of the object dominates the clearance of the sender; the clearance of the receiver dominates the class of the object; the sender is allowed to send to the receiver; and, the receiver is allowed to receive from the sender. An association exists between two subjects if both the last two hold. Note that no operation changes the classification of an object. A Formal Top Level Specification (FTLS) has been produced of the security-critical functions of the NSD, as a Gypsy procedural model of parallel processes communicating via buffers. GVE has been used to prove its security properties; due to the distributed nature of the mediation, this was fairly complex, and one 'obviously true' lemma was beyond the capabilities of GVE. The FTLS is being extended to cover the NSC, and needs further extension to cover communications between (trusted) multilevel hosts. The FTLS of such hosts may be required. It is hoped by the authors that the FTLS of the network could be utilised by designers of secure multilevel hosts, so that statements about end-to-end security can be made #ABSTRACT#558# This Datapro report reviews the criteria that affect the vulnerability of password systems, which are listed as length, lifetime, source, ownership, distribution, storage, entry, tranmission and authentication period. The report recommends careful evaluation of any password system, together with a periodic review procedure of both the system itself and its usage. #ABSTRACT#559# Note: Introduction: System Safety Engineering is the application of scientific and Systems Engineering methodology and management techniques to minimize risk in a product. Software safety is the extension of that discipline into software. Significant differences exist between the traditional safety approach to hardware control and failure modes and safety's new approach to software control and failure modes. While the management shell existed, there were few analysis techniques which were applicable five years ago. Today the safety management shell is being successfully integrated into the software realm and several analysis techniques have nearly been perfected, showing independently repeatable results. The current iteration of improvement involves determining the type and timing of specific data from software and quality engineers. We are perfecting a process which provides software data which is useful and feeds our analysis and reports in a timely, pro-active fashion, rather than "oh, by the way I need it yesterday" requests for data. The current analysis techniques are labor intensive. The next iteration in perfecting the process involves reaching further for active design techniques and efficient analysis techniques. I present this paper to acquaint people with Software Safety Engineering and call upon computer security engineers to call out those design and analysis techniques you possess in your repertoire which might assist us in doing our job better. #ABSTRACT#560# Note: In essence McLean has extended the basic Bell/LaPadula framework in two directions to yield an algebra and a lattice of models. The first extension is to introduce the notion of subjects able to change the clearances of subjects, and the classifications of objects. The second extension allows the formulation of n-person rules. The fact that both these extensions form an algebra, and a lattice wrt the Boolean operators is, apart from theoretical interest, potentially useful to the makers of policy models. More complex models can be constructed by combining simpler models. In a little more detail the development runs as follows: start with the Bell/LaPadula framework of subjects, objects, finite lattice, and access modes. To this are added functions representing which subjects can alter the clearances of which subjects and alter the classifications of which objects. By considering the space of such functions we form a set of models. It is easily shown that these form a partially ordered set. The Boolean operators ð, ð and ' (complement) can be applied to this set to form a (closed) boolean algebra. The second, further extension is to include the notion on n-person rules, where certain access modes to objects are granted only when n subjects request it simultaneously. This is achieved simply by replacing the set of subjects S by its power set less the empty set ð(S)-{ð}. The resulting set of models again form an algebra with respect to the operations ð, ð and '. Unfortunately, this set contains models representing 'bizarre' policies. These can be excluded but with the result that the new set fails to form an algebra; it does, however, continue to form a distributive lattice under ð and ð. Indication is given of how this framework could be applied to DAC instead of MAC. The ideas presented are interesting and potentially useful, particularly to the builders of policy models. Some pleasing mathematics is presented but on the whole the session left a feeling of disappointment. The title and author rather led one to expect something rather deeper and more sweeping. In fact this work rests heavily on Bell/LaPadula and so carries forward many of its deficiencies. Indeed, somewhat curiously, McLean launches into a critique of Bell/LaPadula only to resign himself to it in what follows. An interesting feature of the paper is that it represents another illustration of the concerns for the mathematical properties of sets of models rather than dealing just with the properties models in isolation. This indicates the potential for the application of category theory to security models. A general framework is developed in which various mandatory access control security models that allow changes in security levels can be formalized. These models form a Boolean Algebra. The framework is expanded to include models that allow n-person rules necessary for discretionary access controls in an industrial security setting. The resulting framework is a distributive lattice. #ABSTRACT#561# A general framework is developed in which various mandatory access control security models that allow changes in security levels can be formalized. These models form a Boolean Algebra. The framework is expanded to include models that allow n-person rules necessary for discretionary access controls in an industrial security setting. #ABSTRACT#562# A method for evaluating security models is developed and applied to the model of Bell and LaPadula. The method shows the inadequacy of the Bell and LaPadula model in particular, and the impossibility of any adequate definition of a secure system based solely on the notion of a secure state. The implications for the frutifulness of seeking a global definition of a secure system and for the state of foundational research in computer security in general, is discussed. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 123 - 131 This is a thoughtful reassessment of the Bell & LaPadula security model, maintaining that the model is inadequate to bear the weight the computer security community has placed on it. Attention is drawn to the crucial role of the tranquillity property, which prohibits changing the security level of an active subject; this is dropped from the later formulations of B-LaP. McLean's counterexample, 'system Z', which is obviously insecure and yet conforms to B-LaP has given rise to a lot of controversy over the networks in the last year, and revealed much confusion over the status of the tranquillity property, or more generally, exactly what B-LaP means. McLean argues that uncritical acceptance of the model, and the fact that it is in danger of becoming enshrined in official doctrine, are harmful to deeper understanding and will impede progress. The model has now outlived its usefulness. The moral is that we should not look for some single essence of the concept of security, but rather accept that there may be several concepts which bear only a family resemblance. Thus we should look at each application separately and adopt the relevant concept. #ABSTRACT#563# Note: A most valuable and interesting paper, and winner of one of the two awards for best papers. Various information-flow oriented security models are criticised, as failing to correspond sufficiently well to intuitive notions of security, and a new model put forward. The Bell and Lapadula model is re-examined, and found good. Sutherlandðs Nondeducibility model is criticised on two grounds: „ It is bi-directional (prohibits flows from low to high as well as high to low). Thus it expresses a ðcompartmentalisationð policy rather than a true ðsecurityð policy. „ It protects high-level inputs only, that is, all high-level outputs are presumed derived from high-level inputs. Examples are given to motivate this concern. Firstly there is the generation of high-level cryptographic keys from low-level seed-numbers. More generally, an expensive (ðresource-intensiveð) computation may produce high-level (or high-value) outputs, to be protected, derived from low-level input. Bi-directionality is avoided by taking time into account, and saying that information flows from H to L only if H assigns values to objects in a state which precedes the state in which L makes its assignment. This leads to a first approximation to McLeanðs new model. Advantages claimed are: not bi-directional, rules out systems in which low-level users can gain probabilistic knowledge of high-level events even if they cannot rule out any high-level event as impossible. Finally, under a suitable interpretation, rules out timing channels. The next consideration is that this model is too strong: does not distinguish between purely statistical correlations between H and L and causality. Consider ðstrong auditingð, where a high-level audit record must be written before each write to a low-level object, and the audit record contains a copy of the low-level data about to be written. Here the low objects are apparently tracking the values of high objects (audit records). This is a statistical correlation, not causal (the high objects do not cause the low objects to be what they are), not insecure. This leads to McLeanðs Flow Model, as follows. Let L be an assignment of values to low objects in a given state. The probability of L, given the sequences of high and low assignments in all preceding states, must equal the probability of L given only the sequence of low assignments in all preceding states. Next Goguen and Meseguerðs Noninterference model, and McCulloughðs generalisations to nondeterministic systems are considered. Generalized Noninterference has two problems: „ As with Nondeducibility, protecting high-level input is not always sufficient to protect high-level output. „ Any extension to it concerned with protecting high-level outputs must adequately model causal dependencies to distinguish between statistical correlations among outputs which are security-violations and those which are not. To overcome these problems, a change to Noninterference or its descendants is advocated: not to the syntactic form of the model but to its assumptions and interpretation of its primitives. It is to be assumed that any high-level output to be protected cannot be generated from low-level input data unless that data has been operated on by a high-level program, which is itself a kind of high-level input. Thus we are back to protecting only high inputs again. The final section of McLeanðs paper is concerned with the Bell and Lapadula model (BLP) and its relation to noninterference. Although BLP is a purely formal model with no interpretation prescribed for its primitives (e.g. ðread-accessð), with the customary interpretations it is equivalent to Generalized Noninterference, and intuitively treats causality well. If this is so why is covert channel analysis necessary? To make sure of appropriate interpretations of the BLP primitives. That is to say, we are concerned with the mappings of models to systems. Afterthought: McCulloughðs motivation was explicitly the desire for a compositional property. It isnðt clear at the moment whether McLeanðs formulation is compositional, or what it would take to prove it. We develop a theory of information flow that differs from Nondeducibility's, which we see is really a theory of information sharing. We use our theory to develop a flow-based security model, FM, and show that the proper treatment of security-relevant causal factors in such a framework is very tricky. Using FM as a standard for comparison, we examine Noninterference, Generalized Noninterference, and extensions to Noninterference designed to protect high -level output, and see that the proper treatment of causal factors in such models requires us to consider programs as explicit input to systems. This gives a new perspective on security levels. The Bell and LaPadula Model, on the other hand, more successully models security-relevant causal information although this success is bought at the expense of the model being vague about its primitives. This vagueness is examined with respect to the claim that the Bell and LaPadula Model and Noninterference are equivalent. #ABSTRACT#564# Information flow models are usually conceived in terms of requirements on system traces, while verification that a system satisfies information flow requirements is usually done in terms of a state machine specification. The necessary translation from one model to another may result in a loss of understandability and expressiveness. Recently McLean has pointed the way to a solution to this problem by showing how a language based on traces of procedure calls may be used to reason about security, and how one may prove that a program satisfies a specification written in that language. The language that he uses, however, does not easily lend itself to specification of composition of communicating processes. In this paper we modify the language so that it is possible to specify the composition of systems. We also describe several different information flow properties analogous to properties that have been defined for other systems and discuss their composability. #ABSTRACT#565# This paper presents a secure algorithm to allow representatives of organisations to exchange matching credentials without having to consult their parent organisations; the algorithm ensures that information about the secrets does not pass between the parties if they do not match. Cryptographic techniques, based on the Diffie-Hellman protocol for secure key exchanges are used. Each user knows the public key of each organisation, and the private key of his own; the protocol starts by both parties exchanging signed messages verifying their organisational affiliation, containing a function of their credentials, and establishing an encryption key. This key is used for an acknowledge handshake, and then for a final pair of messages in which users exchange exponentials calculated from their own credentials and the supplied value derived from the other's credentials. The protocol is designed not just to protect the users from outside parties, but also from each other, so that one side cannot discover a match without revealing the fact to the other. The security of the protocol depends on each party protecting their private keys, and on the difficulty of factorising large numbers and of finding logarithms in multiplicative groups. The paper presented itself as an improved solution to a problem addressed by a paper at the 1985 IEEE symposium on security and privacy, the difference being that the new algorithm does not require a third party to be online at all times. However, there are sufficient differences to mean that new algorithm is best considered as a solution to a separate problem. #ABSTRACT#566# Note: The Brewer-Nash model was motivated by the requirements of the UK Financial Services Act for preventing one companyðs sensitive information being passed to another company and for reducing the opportunities for insider trading. It formalises these Chinese walls in a security model. The paper applies the ideas in this model to the old and thorny problem in multilevel security of aggregation. The simplest example of this is the NSA ðphone book where individual entries are not classified but the entire book is. Unlike in the original Brewer-Nash model, sufficiently cleared people may have access to the entire ðphone book. The access denial on aggregation is not absolute, but the sensitivity of the data increases on aggregation. A useful non-military example given was where the budget for departments is not as sensitive as the budget for an entire organisation. The solution presented in this paper is to preserve a history of objects accessed by each subject. The objects accessed imply a minimum sensitivity level to which accessing subjects should be cleared. After prolonged use, certain systems where new data continually arrives for processing could be rendered inoperable. No description was given of any means of ensuring the continuous use of the system, for example by deleting objects in a subjectðs history after a certain time. Unusually, the paper had a rejoinder built into the program. Dorothy Denning argued that aggregation is an abstract problem which is man- made. Since the problem is artificial this model (although a good one) brings out the ugliness of the requirements. She said that users must have access to all information for which they are responsible and that they should not be given access to information for which they have no responsibility. The assignment of responsibility was not a matter of picking up the data at a userðs request as described by the paper but one of deliberate assignment. The latter process is one which is already covered by current models with DAC or a change of user clearance. In the ensuing extended question and answer session the distinction between strategic and tactical information was brought out. Strategic information was more valuable because it enables one to derive the tactical information more readily than in deriving the strategic information from the tactical. It was suggested that the protection of the different types of data should be such that the cost of obtaining the strategic data was equivalent to the cost of obtaining all the tactical data. An analogy was drawn with cryptography where it was asserted that given enough cipher text (tactical data) one could deduce the clear text (strategic data) and that the strength of mechanism had to be appropriate for the two types of data and their availabilities. Finally, we were reminded that computers cannot take the full picture of who has access to what information within an organisation so the histories kept within a computer are likely to be inadequate. In this paper we show how the Brewer-Nash Chinese Wall model can be extended to a policy for handling the aggregation problem in a multilevel context. We derive a lattice-based information flow policy that can be integrated into both the multilevel and Brewer -Nash context. We use this information flow policy to develop a security policy described in terms of labeled subjects accessing labeled objects that will allow us to construct a system that prevents users from accessing aggregates that they are not cleared to see. #ABSTRACT#567# The integrity lock architecture provides a means of constructing a secure database management system with a relatively small amount of trusted code, using a trusted filter which verifies the integrity of security labels on data from an untrusted DBMS by computing cryptographic checksums. However, since the trusted filter can only check whether or not an individual item of data has been tampered with, and not whether or not that item is a correct answer to a particular database query, a covert channel exists through which a Trojan Horse in the DBMS can leak classified information by encoding it in various innocuous queries. In this paper we discuss a possible solution to this covert channel problem for message systems. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 212 - 218 In this paper the method of integrity locks is applied to the hierarchical data structure of NRL's Secure Military Message System. The ideas in this paper are worth further investigation, but increasing the complexity of the integrity lock architecture increases the diversity of covert channels, the effect of inefficiency of cryptography, the difficulty of key management and the number of additional checks in the trusted filter. As Dorothy Denning pointed out, it might be simpler to have a trusted message handling system in the first place. #ABSTRACT#568# In this paper we describe a formal specification language and verification technique for analyzing key management protocols, and we introduce a prototype verification tool that can be used to apply this technique. We formally specify and verify a protocol intended for use in the management of resource sharing, and we show how the use of our techniques led to the discovery of a flaw that could be exploited by an intruder to convince a user of the system that he has obtained a service when he actually has not. #ABSTRACT#569# Note: The security of a cryptographic system is dependent on its cryptographic algorithms, their implementing hardware, and its communications protocols. This paper considers how techniques used in the analysis of term-rewriting systems may be adapted to automated analysis of cryptographic protocols. Consider a network of users, taking part in a cryptographic protocol, having the capability of performing a fixed set operations on data. Although these operations are undefined, certain properties that can be defined algebraically are required (e.g. decryption is the inverse of encryption). The results of operations can be represented symbolically as words in an algebraic system. A cryptographic protocol can be thought of as a set of input data dependent rules. Assume a penetrator has complete control of the communications network; he can analyse, alter or destroy traffic. Assume, however, he knows nothing about the cryptosystem except a set of algebraic properties. His goal is to obtain secret words, i.e. he is trying to determine, in the term-rewriting language, whether there are words that reduce to a secret word. Analysis is a two stage process. Consider the set of insecure system states, then work backwards to show that none of these states can be reached from any secure initial state. There was agreement that there is no rigorous way of establishing the complete set of insecure states. Other difficulties are finding all states from which a given state is immediately reachable, and analysis may lead to an infinite regression. To establish whether a penetrator can derive a word of a particular form, the output of each of the rules defining the protocol are considered and relevant substitutions obtained. General conclusions are drawn about what he originally needed to know to achieve his aim. This process of deriving substitutions is known as ðnarrowingð, a technique for solving in equational systems defined by term-rewriting languages. An inductive argument can be used to prove that a penetrator cannot know any words in the language. Show that, in order for him to learn a word, he must already know another word, and that he did not initially know any words. An analysis of the IBM Key Management Protocol is presented in the paper, along with intended future research and comparisons with other work. The presentation was short, succinct and, in general, well accepted. #ABSTRACT#570# It is argued that techniques for proving the correctness of hardware designs must use abstraction mechanisms for relating formal descriptions at different levels of detail. Four such abstraction mechanisms and their formalisation in higher order logic are discussed. 2T615. #ABSTRACT#571# Note: This paper discusses many of the problems associated with the use of passwords and describes a number of ways in which password- based controls can be compromised or avoided. It is a short paper with no new ideas and not exhaustive in its coverage, but it is a quite readable introduction. No references. #ABSTRACT#572# This is the standard reference given for Ethernet, a baseband mode local area network designed at the Xerox Palo Alto Research Center. Ethernet was designed as a suitable communications system on which distributed computer systems could be based. Ethernet is a broadcast bus-type of network whose medium is a coaxial cable. The designers attempted to make the network as efficient as possible by reducing the amount of system bandwidth wasted through packet collisions. After characterising local area networks the paper gives a brief system summary and lists its design principals, one of which is for ease of expansion. It classifies the topology of an Ethernet as a tree, describes the requirement for cooperation amongst stations, explains that broadcast packets as well as individually addressed ones are allowed and elaborates on the network's reliability and the mechanisms used to provide its packet service. A description is given of hardware and network packet structure details. It is then shown that expansion can be accomodated in the three principal areas of signal cover (using packet repeaters), traffic cover (using packet filters) and address cover (using packet gateways). A semi-mathematical evaluation of performance is then given, followed by a mention of some higher level protocols (an Ethernet file transfer protocol in particular). #ABSTRACT#573# Many of today's network products are based on the client-server distributed network model. This client-server model was analyzed from a security perspective and an expanded client-server model which includes security-relevant properties was developed. As the next step in developing a trusted client-server network, a network-oriented security policy was produced. The various services provided on the distributed network map elegantly into NTCB partitions producing an easily specified system architecture and simplifying the task of resource protection. This approach also allows the NTCB interface to be easily specified since the interface is defined by the network protocols used to access the individual services. #ABSTRACT#574# This paper describes the sort of security model that is likely to be a good starting point for an A1 system. #ABSTRACT#575# For formal methods people with a strong mathematical background. #ABSTRACT#576# This paper gives a summary and some examples of the way in which the TCSEC (Orange Book) might be applied to networks. It is quite a good overview of issues in network security. The speaker noted that the TCSEC working group had changed its view somewhat since the paper was produced. 2T522. #ABSTRACT#577# Describes the verification of a PDP-11/45 security kernel. The kernel is described by a hierarchy of specifications of decreasing abstraction: Bell and LaPadula formal security model; formal specification of the kernel; algorithmic specification written in some high level language; and, the hardware and software machine. The aim is to verify the equivalence between adjacent layers in this hierarchy. This paper concentrates on the verification of the security model and the formal specification. The kernel is specified by its state (a set of objects) and a set of functions that operate on the state. The functions are defined by the state transition they cause. The problem of covert channels being supported by the kernel is discussed. The solution given is to ensure that all state variables within the kernel are objects in the security model sense. Then the paper interprets what the security policy means in terms of the formal specification. Finally, an outline of the proof that the DELETE function conforms to the star property is given. This interesting description of security verification gives the flavour of how such verifications should be organised. #ABSTRACT#578# Techniques for detecting covert channels are based on information flow models. This paper establishes a connection between Shannon's theory of communication and information flow models, such as the Goguen- Meseguer model, that view a reference monitor as a state-transition automaton. The channel associated with a machine and a compromise policy is defined, and the capacity of that channel is taken as measure of covert channel information rate. IEEE Comp. Soc. Proc 1987 Symp. Security and Privacy, pp. 60 - 66 A most interesting paper. Security-properties such as described by the Goguen-Meseguer non-interference model or the Sutherland deducibility model are formally related to the Shannon theory of communication- channel capacity. Under certain assumptions about probability-distribution of inputs, it can be shown that channel capacity is zero, which we would naturally regard as as good as non-interference. However, the converse does not hold: noninterference is not a necessary condition for zero channel capacity; it is simply a sufficient condition. Consequently, non-interference is pessimistic: it implicitly makes the worst-case assumption that inputs from all users other than the one under consideration could be known to or controlled by the attacker. If a source of inputs X interferes with a sink of outputs Y, the amount of information transmitted from X to Y depends on the distribution of inputs from V (sources other than X). Thus if V is constant, channel capacity is maximum. An example is given in which X does interfere with Y but X and Y are statistically independent and thus no information flows - channel capacity being zero. In subsequent discussion, two points emerged. Firstly, that work is under way to actually measure some of these distributions, for example, by logging all system calls under Unix for a period of 3 days. #ABSTRACT#579# A denial-of-service protection base is characterized as a resource monitor closely related to a TCB, supporting a waiting-time policy for benign processes. Resource monitor algorithms and policies can be stated in the context of a state-transition model of a resource allocation system. #ABSTRACT#580# A multilevel object-oriented system can be implemented on a conventional mandatory security kernel. Each object is assigned a single security level that applies to all its contents (variables and methods). The informal security policy model includes properties such as compatibility of security level assignments with the class hierarchy. The representation of integrity constraints and classification constraints is illustrated. #ABSTRACT#581# Note: This paper describes the cascading problem, and claims that a simple nesting property is sufficient to prevent cascading. At the conference, however, the author presented some more recent findings which indicate that all of the statements made in the paper may not necessarily be true. In particular, a example was presented which shows that cascading is possible in some cases where systems have overlapping partially ordered levels, contrary to a statement in the paper. This was a most interesting presentation, and the paper appears quite readable, in spite of being quite mathematically based. #ABSTRACT#582# This report examines five leading products: the Atalla confidante, a DES-based, PIN-protected calculator-like device developed for low- volume EFT; the Enigman Logic Safeword, a small plug-in device with a coded identity used in conjunction with a special decode device; the Gordian Systems Access Key, which uses an optical reader to pick up the challenge direct from the user's screen; the Security Dynamics SecurID, a roughly credit-card sized device that uses a time synchronisation method rather than a displayed challenge; and the Sytek PFX PassPort, another PIN-protected calculator-like device, which offers DES and 14 other crypto algorithms. #ABSTRACT#583# An access control mechanism based on boolean expression evaluation, BEE, is presented. This mechanism allows the implementation of customer-specified rather than vendor-specified security policies. The mechanism enables one to easily implement such conventional mechanisms as access control lists, named access control lists, user groups, user attributes, user capability lists, and user roles. Additional access restrictions based on time, day, date, location, load average, or any customer-supplied function can be incorporated into access decisions. This mechanism can directly express Clark-Wilson triples and it can easily implement policies that are difficult or impossible to implement using the Bell-LaPadula model. #ABSTRACT#584# The intention of the National Software Works (NSW) was to provide ARPANET programmers with a unified tool kit, distributed over many hosts, and a single user interface with a uniform command language, a global file system and a single access control, accounting, and auditing mechanism. In this way the cost of software production would be dramatically reduced. The system was in regular operation from May 1977. The main components of NSW are: 'MSG', the inter-process message system which supports both generic and specific addressing and three types of communication (messages, connections, and alarms); the file system and works manager, which manages authentication, job creation, file access, and other distributed operating system function; the foreman which is the local run-time system/operating system in individual hosts; and, the file package, which resides on every host #ABSTRACT#585# In a distributed database system, several replicas (copies) of a data object may be maintained at different sites to improve reliability. However, maintaining replicas may also affect the security of the system in terms of secrecy and integrity. Thus, it is natural to integrate reliability and security issues within a replica control protocol. In this paper, we present a secure quorum protocol which integrates a quorum protocol to attain consistency of replicated data and a cryptographic technique to attain security of data. We present two efficient methods for generating quorums which are best suited for the secure quorum protocol. Then, we present an algorithm, called the join algorithm, which is very useful for constructing a large set of quorums and show that the join algorithm may be used to improve the overall security of the secure quorum protocol. #ABSTRACT#586# A method of implementing access control for computer resources is presented, along with examples and possible enhancements. An appropriate application for such resource control can be found in computer operating systems. Thus, the need for resource control is described first, followed by descriptions of some common implementations and the impetus for their development. In light of this discussion, the alternative implementation proposed in this paper will be presented, followed by a discussion of what improvements over the classical implementations are offered. This done, a series of possible extensions are presented. #ABSTRACT#587# Traditional methods of user authentication in distrlbuted systems suffer from an important weakness which is due to the low degree of randomness in secrets that human be- ings can use for identification. Even though weak secrets (passwords and PINs) are typically not exposed in the clear over the communication lines, they can be discovered with off-line brute force attacks based on exhaustive trials. Since such secrets are chosen from a relatively small key space, a determined adversary can try all possible values until a match is found between the trial value and the message recorded from a genuine authentication session. Authen- tication devices like smartcards and token cards offer an attractive solution by providing a user with a cryptograph- ically strong key for authentication. In contrast to pass- words and PINs, the device's key can be chosen from a much larger key space thus making a brute force attack computationally infeasible or, at least, diffcult. In this paper we present a novel authentication method whereby the authentication device (a token card) is used solely to provide a secure channel between a human user and an authentication server (AS). Since the communi- cation channel is secured by the card, the user can stlll utilize weak secrets for authentication purposes, but, with- out any risk of exposure. Furthermore, the card's and the user's secrets are mutually independent, i.e., the card is not associated with any particular user. Since the card is impersonal, it can be freely shared by several users. This eliminates the high cost of administration which is typi- cal of existing designs requiring fixed user-device relation- ship. Moreover, our method does not require any coupling between the token card and the workstation (e.g., a gal- vanic connection) which would be dificult to implement on a global scale and retrofit onto existing equipment. #ABSTRACT#588# Note: Referenced in: Leonard, Timothy E., 'Specification of Computer Architectures: Survey and Annotated Bibliography'. ( Cambridge University Computer Laboratory Technical Report No. 188). #ABSTRACT#589# Note: A framework is presented with which to discuss the problems of inference that occur in multilevel database systems. It is suggested in the paper that, due to the inherent complexity of inference detection, this framework be the base for a set of computer based tools for the detection of inference. The framework is based on a universe of discourse which is held to contain all relations specified in the database and also all relationships and constraints external to the database that a potential user could know. This universe is potentially infinite and it is thus not possible to ensure that all relevant external information has been captured. Data objects in this universe are related by inference. Given a data object it is possible to infer (possibly partial) information about other data objects. Characterising inference allows the description of the sphere of influence of a (core) set of data objects as being all objects that can be inferred from this core data. Safety can be defined in terms of inference and sphere of influence. A data object is safe if, from it, you can infer nothing of a higher classification. A classification level is safe if the sphere of influence of the objects of that classification level contain no objects of a higher classification - a sufficient condition for this is that the sphere of influence is a fixed point for those objects. Safety utilises forward chaining of inference: what can be inferred from something. Inference channels are backward chaining: from what can we infer something. An inference channel for a data object details data objects from which that object can be (partially) deduced. Using the language of inference, spheres of influence, safety and inference channels it is now possible to disuss inference and its effects on multi-level database systems. The paper describes how, once potential inference channels have been recognised, they can either be removed, their effect reduced or be monitored. This paper is closely related to that presented by T.ðH.ðHinke, entitled 'Inference Aggregation Detection in Database Management Systems' (pp. 96-106 of the proceedings). The potential for logical inference of high level information based upon lower level visible data presents an interesting and challenging threat to multilevel security. Such compromises of security are rather novel since they circumvent traditional security mechanisms and rely on a user's knowledge of the application, which is external to the security layers of the system. The potential for such inferences, and the multiple consequences of a corrective action, substantially complicate the task of classifying the data in a secure manner. Computer-based tools will be needed to assist in this process, especially when multilevel databases of substantial size and complexity are considered. Heretofore, the problems of inference and security have been amorphous and difficult to circumscribe. This paper proposes a framework for studying these inference control problems, describes a representation for relevant semantics of the application, develops criteria for safety and security of a system to prevent these problems, and describes the functionality of the proposed classification tool in terms of a scenario for its use. #ABSTRACT#590# Note: The paper was presented at the Conference but copies issued separately and not as part of the Proceedings. This paper was mainly concerned with digital telephone systems for voice and data transmission, and the types of attack which may be made on them. These include transmission confidentiality, transmission integrity, denial of service, system software integrity and system hardware integrity. The last of these is somewhat more likely to be a problem in a telephone system than a computer system, because of its wide geographic distribution. It is pointed out, however, that this could become a problem in computer systems, since, if chip- production facilities are available, it is possible to manufacture 'replacement' chips which could be installed in target machines, unknown to their owners. These chips could perform additional covert functions whilst mimicking the originals. Most of this paper is specific to telephone-like networks, but the suggestion of 'spoof chips' appears to be significant. These chips could be made to carry out many covert functions, the easiest of which to manufacture is the 'chip bomb'. This could be designed to generate a denial of service attack at a specified time, or, for example, by radio command. Many other possible variants of this idea could be used. #ABSTRACT#591# This looks at the way the UNIX passsword protection mechanism has developed over the years, in response to attacks. It started off by holding password information in a heavily protected file, then one-way encryption was used. This is vulnerable to attacks through trying likely passwords; dictionaries can be built containing candidate passwords and their encrypted forms. Adopting DES - which is slow in software - improved security; use of DES chips in an attack is avoided by modifying the algorithm slightly. Other improvements were to avoid predictable passwords by warning users if they chose a bad one, and by salting the password before encryption with a 12-bit number stored with the encrypted passwords - this 'seed' is chosen randomly when the password is set up. 2T70. #ABSTRACT#592# This document describes a software system provided to meet a requirement for microcode generation. The system is configurable with respect to target hardware, and microprogramming is enables in a higher level language than traditional assembler programming. #ABSTRACT#593# This document describes a high level micro-programming language, that is part of a microcode development system. The output of the compiler is a regular algebra to which homomorphic transformations can subsequently be applied. #ABSTRACT#594# We will investigate the effects of noise upon a simple timing channel. Shannon's information theory is used to quantify the resulting information flow across the channel. In particular we study how a probabilistic response time to a query by a low user affects the mutual information and channel capacity. We obtain a result of Millen's as a special case. #ABSTRACT#595# We consider an optimization problem in calculating the bandwidth of a covert timing channel. Special function techniques and numerical analysis are used to analyze the bandwidth. This paper generalizes previous work by the authors and was motivated by an example of J. Millen. #ABSTRACT#596# This report identifies various computer fraud techniques, and suggests ways of investigating a computer crime and deals with the criminals. It is based on a section of 'Computer Security Handbook: Strategies and Techniques for preventing data loss and theft', Prentice-Hall (1986). #ABSTRACT#597# This paper proposes a reference framework to help improve the effectiveness of information security management. The framework is intended as a standardized vehicle that can be used by both business and security managements to identify and prioritize information security requirements on the basis of the intended use of the information, the value priority of the information, and the critical security factors for that information. The paper also suggests that a serendipitous benefit resulting from the use of the proposed framework could be a better understanding of the present and potential use of an organization's information assets for competitive advantage. #ABSTRACT#598# This paper describes CORE, a method for Controlled Requirement Expression. The CORE method has been defined to fit into a set of standards and procedures produced by Systems Designers Limited. A mapping has been defined from the CORE diagrammatic notation into the terminology of the automated aid PSL/PSA (ref.1) CORE is applicable to description of dynamic aspects of many types of system (i.e. not just computer systems). Current applications include: specifying requirements for a new avionics system; a description of the total project organisation, standards and procedures for the software life-cycle; description of the requirements for an automated aid for system description. CORE is supported by a diagrammatic notation whose features derive from several widely used specification and design diagrammatic notations. The notation can be applied to the description of both requirement and design. This paper describes its application to requirement. 2T625. #ABSTRACT#599# Note: Introduction: This paper seeks to identify common issues relating to the use of security labels within the secure ODA and secure POSIX environments. The underlying security concepts of the two standards are discussed and mutual requirements highlighted. After an analysis of existing security labels, we propose an optimum generic security label. Finally, we discuss how a secure system may utilize the security label capabilities of both ODA and POSIX to provide appropriate sensitivity label protection for documents and information labels for document handling restrictions. This paper represents the views of the authors and does not represent the views of British Telecom, Alcatel nor those of the ISO/IEC, ECMA or IEEE standardization bodies. #ABSTRACT#600# A cryptographic scheme can be used for controlling access to information, since any user who does not have a proper key can not decipher. But for this purpose, a user would have to manage a huge number of keys when he tries to communicate with a lot of people. The practical utilization method of access control by cryptography is discussed in this paper. We suppose a typical organizational structure called hierarchical group oriented structure. After that, we propose a hierarchical group oriented key management method (HGK method) based on the multiple keys generated from the combination of pieces, and describe that this method is very desirable in terms of reducing the numbers of keys required for each user in the hierarchical group oriented structure. #ABSTRACT#1000# Classification constraints are rules for assigning access classes to data when they are entered into a database. In order that a given set of constraints specify meaningful classes, they should be consistent, that is, not define conflicting classes for the same data. This paper gives algorithms for checking the consistency and completeness of a set of classification constraints defined on a database schema. The techniques use computational geometry to compute intersecting regions in a multidimensional space, where each region is defined by a classification constraint or integrity constraint. pp. 196 - 201 This paper follows on from the previous year's paper where classification constraints are applied to database views. It argues that: „ classification constraints must be considered with integrity constraints, and „ classification constraints must be simple otherwise nobody will understand them or their interactions with the other constraints. However, the need for consistency checks arises from the resultant classification by each rule being given as a single value. Since not all rules would be expected to be equally important in every case there seems to be no reason why all rules applying to an object should result in the same classification. Therefore there is no use for the consistency checks if the least upper bound of all the classifications from the rules is taken. Completeness could be covered by a default rule, for example that all objects should be classified according to their source. #ABSTRACT#1001# We propose a secure communication architecture for distributed systems that puts security below the transport level, and uses host- to-host rather than process-to-process secure channels. We argue that this provides the same level of end-to-end security as putting security at higher levels, and that it can simplify and improve the performance of transport protocols. The architecture is designed for very large distributed systems, which in general have security requirements beyond those of LAN-based systems. #ABSTRACT#1002# We propose a secure communication architecture for distributed systems that puts security below the transport level, and uses host- to-host rather than process-to-process secure channels. We argue that this provides the same level of end-to-end security as putting security at higher levels, and that it can simplify and improve the performance of transport protocols. The architecture is designed for very large distributed systems, which in general have security requirements beyond those of LAN-based systems. This paper presents an Authenticated Datagram Protocol (ADP) operating below the transport level for use in high-speed distributed systems where: „ there is no single administrative authority able to provide a universally-trusted name or key service and able to punish offenders; and, „ not all system-level components are equally trusted. A system is considered as a series of hosts, each with an operating system kernel, and a set of security principals, or owners, each with a private/public key pair. The paper specifies what it means by 'kernel secure'. It then identifies the conditions under which it can guarantee that a message a kernel is delivering to one of its processes came from a process for a given owner, and that the message was aimed at the 'port' set up by the receiving process. The conditions surrounding the guarantees it offers to the sender are also established. The paper concludes with a comparison with other architectures such as the Birrell RPC Protocol.