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 number generator for creating address space localization randomization offsets to protect memory addresses to processes from exploration, storing users' password securely and creating cryptographic keys. The paper proposes a CSPRNG called KCS-PRNG which produces non-reproducible bitstreams. The proposed KCS-PRNG presents an efficient design uniquely configured with two new non-standard and verified elliptic curves and clock-controlled linear feedback shift registers and a novel method to consistently generate non-reproducible random bits of arbitrary lengths. The generated bit streams are statistically indistinguishable from true random bitstreams and provably secure, resilient to important attacks, exhibits backward and forward secrecy, exhibits exponential linear 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 many specimina of mathematical content. Its goals and syntactic ideas inspired Th. Coquand and G. Huet to develop the calculus of constructions, CC, which was one of the first widely used interactive theorem provers and forms the basis for the widely used Coq system. The original syntax of Automath is not easy to grasp. Yet, it is essentially based on a derivation system that is similar to the Calculus of Constructions (`CC'). The relation between the Automath syntax and CC has not yet been sufficiently described, although there are many references in the type theory community to Automath. In this paper we focus on the backgrounds and on some uncommon aspects of the syntax of Automath. We expose the fundamental aspects of a `generic' Automath system, encapsulating the most common versions of Automath. We present this generic Automath system in a modern syntactic frame. The obtained system makes use of {\lambda}D, a direct 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 same length-preserving transduction, starting with a sweep on the input string and then iteratively sweeping on the output of the previous sweep. The IUFST accepts the input string by halting in an accepting state at the end of a sweep. We consider both the deterministic (IUFST) and nondeterministic (NIUFST) version of this device. We show that constant sweep bounded IUFSTs and NIUFSTs accept all and only regular languages. We study the state complexity of removing nondeterminism as well as sweeps on constant sweep bounded NIUFSTs, the descriptional power of constant sweep bounded IUFSTs and NIUFSTs with respect to classical models of finite-state automata, and the computational complexity of several decidability questions. Then, we focus on non-constant sweep bounded devices, proving the existence of a proper infinite nonregular language hierarchy depending on the sweep complexity both in the deterministic and nondeterministic case. Though NIUFSTss are "one-way" devices we show that they characterize the class of context-sensitive languages, that is, the complexity class DSpace(lin). Finally, we show that the nondeterministic devices are more powerful than their deterministic variant for a sublinear number 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. An efficient diagnosis is crucial for a multiprocessor system. The BGM diagnosis model is a modification of the PMC diagnosis model, which is a test-based diagnosis. In this paper, we present a specific structure and propose an algorithm for diagnosing a node in a system under the BGM model. We also give a polynomial-time algorithm that a node in a hypercube-like network can be diagnosed correctly in three test rounds under the BGM diagnosis model.