Volume 185, Issue 4

1. On Random Number Generation for Kernel Applications

Kunal Abhishek ; George Dharma Prakash Raj E.
An operating system kernel uses cryptographically secure pseudorandom numbergenerator for creating address space localization randomization offsets toprotect memory addresses to processes from exploration, storing users' passwordsecurely and creating cryptographic keys. The paper proposes a CSPRNG calledKCS-PRNG which produces non-reproducible bitstreams. The proposed KCS-PRNGpresents an efficient design uniquely configured with two new non-standard andverified elliptic curves and clock-controlled linear feedback shift registersand a novel method to consistently generate non-reproducible random bits ofarbitrary lengths. The generated bit streams are statisticallyindistinguishable from true random bitstreams and provably secure, resilient toimportant attacks, exhibits backward and forward secrecy, exhibits exponentiallinear complexity, large period and huge key space.

2. Characteristics of de Bruijn's early proof checker Automath

Herman Geuvers ; Rob Nederpelt.
The `mathematical language' Automath, conceived by N.G. de Bruijn in 1968,was the first theorem prover actually working and was used for checking manyspecimina of mathematical content. Its goals and syntactic ideas inspired Th.Coquand and G. Huet to develop the calculus of constructions, CC, which was oneof the first widely used interactive theorem provers and forms the basis forthe widely used Coq system. The original syntax of Automath is not easy tograsp. Yet, it is essentially based on a derivation system that is similar tothe Calculus of Constructions (`CC'). The relation between the Automath syntaxand CC has not yet been sufficiently described, although there are manyreferences in the type theory community to Automath. In this paper we focus onthe backgrounds and on some uncommon aspects of the syntax of Automath. Weexpose the fundamental aspects of a `generic' Automath system, encapsulatingthe most common versions of Automath. We present this generic Automath systemin a modern syntactic frame. The obtained system makes use of {\lambda}D, adirect extension of CC with definitions.

3. Computational and Descriptional Power of Nondeterministic Iterated Uniform Finite-State Transducers

Martin Kutrib ; Andreas Malcher ; Carlo Mereghetti ; Beatrice Palano.
An iterated uniform finite-state transducer (IUFST) runs the samelength-preserving transduction, starting with a sweep on the input string andthen iteratively sweeping on the output of the previous sweep. The IUFSTaccepts the input string by halting in an accepting state at the end of asweep. We consider both the deterministic (IUFST) and nondeterministic (NIUFST)version of this device. We show that constant sweep bounded IUFSTs and NIUFSTsaccept all and only regular languages. We study the state complexity ofremoving nondeterminism as well as sweeps on constant sweep bounded NIUFSTs,the descriptional power of constant sweep bounded IUFSTs and NIUFSTs withrespect to classical models of finite-state automata, and the computationalcomplexity of several decidability questions. Then, we focus on non-constantsweep bounded devices, proving the existence of a proper infinite nonregularlanguage hierarchy depending on the sweep complexity both in the deterministicand nondeterministic case. Though NIUFSTss are "one-way" devices we show thatthey characterize the class of context-sensitive languages, that is, thecomplexity class DSpace(lin). Finally, we show that the nondeterministicdevices are more powerful than their deterministic variant for a sublinearnumber of sweeps that is at least logarithmic.

4. A Local Diagnosis Algorithm for Hypercube-like Networks under the BGM Diagnosis Model

Cheng-Kuan Lin ; Tzu-Liang Kung ; Chun-Nan Hung ; Yuan-Hsiang Teng.
System diagnosis is process of identifying faulty nodes in a system. Anefficient diagnosis is crucial for a multiprocessor system. The BGM diagnosismodel is a modification of the PMC diagnosis model, which is a test-baseddiagnosis. In this paper, we present a specific structure and propose analgorithm for diagnosing a node in a system under the BGM model. We also give apolynomial-time algorithm that a node in a hypercube-like network can bediagnosed correctly in three test rounds under the BGM diagnosis model.