The Center for Education and Research in Information Assurance and Security (CERIAS)

The Center for Education and Research in
Information Assurance and Security (CERIAS)

Reports and Papers Archive


Browse All Papers »       Submit A Paper »

Formal Verification of Counterflow Pipeline Architecture

Paul N. Loewenstein

Some properties of the Sproull counterflow pipeline architecture are formally verified using automata theory and higher order logic in the HOL theorem prover.  The proof steps are presented.  Despite the pipeline being a non-deterministic asynchronous system, the verification proceeded with minimal time and effort. Because this work is directly associated with the asynchronous processor design technology currently being invesigated in the Labs, this report was printed as a courtesy by Sun Microsystems Laboratories.

Added 2003-09-19

Simple Activation for Distributed Objects

Ann Wollrath, Geoff Wyant, Jim Waldo

In order to support long-lived distributed objects, object activation is required.  Activation allows an object to alternate between periods of activity, where the object implementation executes in a process; and periods of dormancy, where the object is on disk and utilizes no system resources. We describe an activation protocol for distributed object systems.  The protocol features overall simplicity as well as applicability to several different activation models.  We use the Modula-3 network object system as a base for our implementation; while we maike no changes to the marshalling of network object subsystem, we suggest a minor modifacation that could be made to the marshalling of network objects to assist in lazy activation, our preferred activation model.

Added 2003-09-19

Events in an RPC Based Distributed System

Jim Waldo, Geoff Wyant, Ann Wollrath, Samuel C. Kendall

In this report, we show how to build a distributed system allowing objects to register interest in and receive notification of events in other objects.  The system is built on top of a pair of interfaces that are interesting only in their extreme simplicity.  We then present a simple and efficient implementation of these interfaces. Next, we show how more complex functionality can be introduced to the system by adding third-party services.  These services can be added without changing the simple interfaces, and without changing the objects in the system that do not need the functioality of those services. Finally, we note a number of open issues that remain, and attempt to draw some conclusions based on the work.

Added 2003-09-17

The Safe-Tcl Security Model

John K. Ousterhout, Jacob Y. Levy, Brent B. Welch

Safe-Tcl is a mechanism for controlling the execution of programs written in the Tcl scripting language.  It allows untrusted scripts (applets) to be executed while preventeing damage to the environment or leakage of private information.  Safe-Tcl uses a padded cell approach: each applet is isolated in a safe interpreter where it cannot interact directly with the rest of the application.  The execution environment of the safe interpreter is controlled by trusted scipts running in a master interpreter.  Safe-Tcl provides an alias mechanism that allows applets to request services from the master interpreter in a controlled fashion.  Safe-Tcl allows a variety of security policies to be implemented even within a single application, and it supports both policies that authenticate incoming scrips and those that do not.

Added 2003-09-17

A Recursive Session Token Protocol for use in Computer Forensics and TCP Traceback

CERIAS TR 2002-41
Brian Carrier and Clay Shields
Download: PDF
Added 2003-09-12


Paronomasic Puns: Target Recoverability towards Automatic Generation

CERIAS TR 2003-25
Christian F. Hempelmann
Download: PDF

The aim of this dissertation is to create a theory to model the factors, prominently, but not exclusively the phonological similarity, important in imperfect punning and to outline the implementation of this measure for the evaluation of possible imperfect puns given an input word and a set of possible target words. Imperfect, heterophonic, or paronomasic, puns differ from perfect, homophonic puns in that the target is different in sound from the pun. While homophonic puns are interesting for the linguist primarily with respect to their semantics, heterophonic puns present a research issue also to the phonologist, because they use one of two similar sound sequences to stand for both meanings associated with them, for example, bang to denote a noise as well as a financial institution. The specific question here is, how much contrast is possible between the pun and its target to make the latter recoverable, in terms of the semantics, phonology, and syntax of the pun-target pair and its context. The theoretical framework for the phonological part of this project is inspired by a recent version of Optimality Theory (OT), adopted in phonology, because it is able to describe the occurrence of related forms through a selection process from among possible candidate forms more appropriately than derivational approaches can by way of rules operating on one input form and yielding one output form. Taking more parameters

Added 2003-08-22

Optimal Secure Interoperation in a Multi-Domain Environment Employing RBAC Policies

CERIAS TR 2003-24
Basit Shafiq, James Joshi, Elisa Bertino, and Arif Ghafoor
Download: PDF

Multi-domain application environments where distributed multiple organizations interoperate with each other are becoming a reality as can be seen in most Internet-based enterprise applications. Composition of a global security policy that governs information and resource accesses in such environments is a challenging problem. In this paper, we propose a policy integration mechanism that merges security policies of multiple collaborating domains into one unified global access control policy. This global policy ensures that security and autonomy of constituent domains are not compromised due to inter-domain information and resource sharing.

Added 2003-08-19

A Generalized Temporal Role Based Access Control Model for Developing Secure Systems

CERIAS TR 2003-23
James Joshi
Download: PDF

A key issue in computer system security is to protect information against unauthorized access.  Emerging workflow-based applications in healthcare, manufacturing, the financial sector, and e-commerce inherently have complex, time-based access control requirements.  To address the diverse security needs of these applications, a Role Based Access Control (RBAC) approach can be used as a viable alternative to traditional discretionary and mandatory access control approaches.  The key features of RBAC include policy neutrality, support for least privilege, and efficient access control management. However, existing RBAC approaches do no address the growing need for supporting time-based access control requirements for these applications.

This research presents a Generalized Temporal Role Based Access Control (GTRBAC) model that combines the key features of the RBAC model with a powerful temporal framework.  The proposed GTRBAC model allows specification of a comprehensive set of time-based access control policies, including temporal constraints on role enabling, user-role and role-permission assignments, and role activities.  The model provides an event-based mechanism for supporting dynamic access control policies, which are crucial for developing secure workflow-based enterprise applications.  In addition, the temporal hierarchies and separation of duty constraints facilitated by GTRBAC allow the development of security policies for commercial enterprises.  The thesis provides various design guidelines for managing complexity and building secure systems based on this model.  X-GTRBAC, an XML-based policy language has been developed to allow specification of GTRBAC policies.

Added 2003-08-19

Multicriteria Routing for Guaranteed Performance Communications

CERIAS TR 2003-21
Dong-won Shin
Download: PDF

In this thesis, we investigate two routing problems.  The first, which is known as the multiconstraint QoS (quality of service) routing problem, is to find a single path that satisfies multiple QoS constraints.  For this problem, we consider two routing environments: (a) a given source node has detailed routing information provided by a link-state protocol, and (b)  the source node has relatively simple routing information provided by a distance-vector protocol.  First, we develop a greedy scheme, called MPLMR (Multi-postpath-based lookahead multiconstraint routing), for case (a).  MPLMR has an efficient

Added 2003-08-11

An Interactive Conception of the Psychological Refractory Period Effect

CERIAS TR 2003-22
Mei-Ching Lien
Download: PDF

An interactive conception of the psychological refractory period (PRP) effect is proposed on the basis of Hommel’s (1998) two-process approach to account for compatibility effects in the PRP task.  The interactive conception account assumes that response selection has two components.  One component is stimulus-response (S-R) translation, which can occur automatically and simultaneously for both tasks.  The other component is final response selection, which is the locus of the bottleneck and can process only one task at a time.  The account suggests that between-task crosstalk and noncurrent-task response association have strong impacts on S-R translation when there is a contingency between the two tasks.  Six PRP experiments were conducted:  The first three experiments contained no contingency between the two tasks, but the last three did.  Greenwald and Shulman’s (1973) S-R compatible and ideomotor compatible tasks were used in Experiments 1-3, with both responses (R1 and R2 for Task 1 and Task 2, respectively) being required in Experiments 1-2 and only R2 in Experiment 3.  The interactive conception predicts that the PRP effect should be obtained in Experiments 1 and 2 but not in Experiment 3 because the selection of R2 has to wait until the selection of R1 is completed.  A PRP effect was evident in Experiments 1 and 2 but not Experiment 3.  In Experiment 4, the dimensional overlap of the color between the first stimulus (S1) and the second one (S2) was manipulated and participants were instructed to respond to S2 only.  A large PRP effect was obtained for the dimensional overlap condition and a small, but significant, PRP effect for the condition with no dimensional overlap.  Experiments 5 and 6 examined the effect of S1-S2 correlation (high, low, and neutral), as well as spatial correspondence (R1-R2 correspondent and R1-R2 noncorrespondent) in Experiment 6, on the PRP effect.  An overaddictive interaction of S1-S2 correlation and SOA was obtained for both experiments.  A comparison between Experiment 5 and 6 showed no difference in the PRP effect obtained with the three levels of S1-S2 correlation.  However, the effect of correlation tended to be larger at the short SOA in Experiment 6, in which spatial correspondence of responses was manipulated, than in Experiment 5, in which it was not.  Results of these experiments are in agreement with the interactive conception of the PRP effect, in which the contingency between two tasks affects the S-R translation processing, which is distinct from the processing of final response selection.

Added 2003-08-11

Type Matching and Type Inference for Object-Oriented Systems

CERIAS TR 2003-20
Tian Zhao
Download: PDF

Type systems in object-oriented systems are useful tools to ensure correctness, safety, and integration of programs.  This thesis studies the matching of recursive interface types for the purpose of software-system integration and type inference for object types to help reduce bulky type information for programs with flexible type systems. We explore the problem of equality and subtyping of recursive types.  Potential applications include automatic generation of bridge code for multi-language systems and type-based retrieval of software modules from libraries.  We present efficient decision procedures for a notion of type equality that includes unfolding of recursive types, and associativity and commutativity of product types.  Advocated by Auerbach, Barton, and Raghavachari, these properties enable flexible matching of recursive types. We also present results on type inference for object-oriented languages with flexible type systems including features such as read-only field and record concatenation. Read-only fields are useful in object calculi, pi calculi, and statically-typed intermediate languages because they admit covariant subtyping, unlike updateable fields.  For example, Glew’s translation of classes and objects to an intermediate calculus places the method tables of classes into read-only fields; covariant subtyping on the method tables is required to ensure that subclasses are translated to subtypes.  In programs that use updateable fields, read-only fields can be either specified or discovered.  For both cases, we will show that type inference is equivalent to solving type constraints and computable in polynomial time. Record concatenation, multiple inheritance, and multiple-object cloning are closely related and part of various language designs.  For example, in Cardelli’s untyped Obliq language, a new object can be constructed from several existing objects by cloning followed by concatenation; an error is given in case of field name conflicts.  We will present a polynomial-time type inference algorithm for record concatenation, subtyping, and recursive types.  Our example language is the Abadi-Cardelli object calculus extended with a concatenation operator. Our algorithm enables efficient type checking of Obliq programs without changing the programs at all.

Added 2003-08-05

Cryptanalysis

S. S. Wagstaff, Jr.

This is a clear, concise summary of the most important and useful parts of cryptanalysis.

Added 2003-07-18

Aurifeuillian factorizations and the period of the Bell numbers modulo a prime

S. S. Wagstaff, Jr.

We give an algorithm for computing formulas for Aurifeuillian factorzations and study the period of the Bell exponential integers modulo a prime number

Added 2003-07-18

Number Theoretic Calculations

S. S. Wagstaff, Jr.

A clear concise summary of calculations in number theory.

Added 2003-07-18