#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 han