Diversity and fault avoidance for dependable replication systems

In the hot-standby replication system, the system cannot process its tasks anymore when all replicated nodes have failed. Thus, the remaining living nodes should be well-protected against failure when parts of replicated nodes have failed. Design faults and system-specific weaknesses may cause chain reactions of common faults on identical replicated nodes in replication systems. These can be alleviated by replicating diverse hardware and software. Going one-step forward, failures on the remaining nodes can be suppressed by predicting and preventing the same fault when it has occurred on a replicated node. In this paper, we propose a fault avoidance scheme which increases system dependability by avoiding common faults on remaining nodes when parts of nodes fail, and analyze the system dependability.     

Local and global deadlock-detection in component-based systems are NP-hard

Interaction systems are a formal model for component-based systems. Combining components via connectors to form more complex systems may give rise to deadlock situations. We present here a polynomial time reduction from 3-SAT to the question whether an interaction system contains deadlocks.     

Compiling and securing cryptographic protocols

Protocol narrations are widely used in security as semi-formal notations to specify conversations between roles. We define a translation from a protocol narration to the sequences of operations to be performed by each role. Unlike previous works, we reduce this compilation process to well-known decision problems in formal protocol analysis. This allows one to define a natural notion of prudent translation and to reuse many known results from the literature in order to cover more crypto-primitives. In particular this work is the first one to show how to compile protocols parameterised by the properties of the available operations.     

Effective homology of bicomplexes, formalized in Coq

In this paper, we present a complete formalization in the Coq theorem prover of an important algorithm in computational algebra, namely the calculation of the effective homology of a bicomplex. As a necessary tool, we encode a hierarchy of algebraic structures in constructive type theory, including graded and infinite data structures. The experience shows how some limitations of the Coq proof assistant to deal with this kind of algebraic data can be overcome by applying a separation of concerns principle; more concretely, we propose to distinguish in the representation of an algebraic structure (such as a group or a module) a behavioural part, containing operation signatures and axioms, and a structural part determining if the algebraic data is free, of finite type and so on.     

On the security of the verifiably-encrypted signature scheme of Boneh, Gentry, Lynn and Shacham

We discuss the security of the verifiably-encrypted signature scheme of Boneh, Gentry, Lynn and Shacham. It is quite realistic to allow adversaries access to adjudication oracles for different users but the same adjudicator. This presents an extension of the security model considered by Boneh, Gentry, Lynn and Shacham and we describe an efficient attack on their scheme in that model. We then show how to obtain security in this extended model by applying a small modification to their scheme.     

Weak bisimilarity between finite-state systems and BPA or normed BPP is decidable in polynomial time

We prove that weak bisimilarity is decidable in polynomial time between finite-state systems and several classes of infinite-state systems: context-free processes and normed basic parallel processes (normed BPP). To the best of our knowledge, these are the first polynomial algorithms for weak bisimilarity problems involving infinite-state systems.     

An approach to formal verification of human–computer interaction

The correct functioning of interactive computer systems depends on both the faultless operation of the device and correct human actions. In this paper, we focus on system malfunctions due to human actions. We present abstract principles that generate cognitively plausible human behaviour. These principles are then formalised in a higher-order logic as a generic, and so retargetable, cognitive architecture, based on results from cognitive psychology. We instantiate the generic cognitive architecture to obtain specific user models. These are then used in a series of case studies on the formal verification of simple interactive systems. By doing this, we demonstrate that our verification methodology can detect a variety of realistic, potentially erroneous actions, which emerge from the combination of a poorly designed device and cognitively plausible human behaviour.     

A note on the attractor-property of infinite-state Markov chains

In the past 5 years, a series of verification algorithms has been proposed for infinite Markov chains that have a finite attractor, i.e., a set that will be visited infinitely often almost surely starting from any state. In this paper, we establish a sufficient criterion for the existence of an attractor. We show that if the states of a Markov chain can be given levels (positive integers) such that the expected next level for states at some level n>0 is less than n−Δ for some positive Δ, then the states at level 0 constitute an attractor for the chain. As an application, we obtain a direct proof that some probabilistic channel systems combining message losses with duplication and insertion errors have a finite attractor.     

Verifying lossy channel systems has nonprimitive recursive complexity

Lossy channel systems are systems of finite state automata that communicate via unreliable unbounded fifo channels. It is known that reachability, termination and a few other verification problems are decidable for these systems. In this article we show that these problems cannot be solved in primitive recursive time.     

HySAT: An efficient proof engine for bounded model checking of hybrid systems

In this paper we present HySAT, a bounded model checker for linear hybrid systems, incorporating a tight integration of a DPLL–based pseudo–Boolean SAT solver and a linear programming routine as core engine. In contrast to related tools like MathSAT, ICS, or CVC, our tool exploits the various optimizations that arise naturally in the bounded model checking context, e.g.isomorphic replication of learned conflict clauses or tailored decision strategies, and extends them to the hybrid domain. We demonstrate that those optimizations are crucial to the performance of the tool.     

Development methods for trusted computer systems

Conclusion Well-designed computer systems can be safer than hardwired alternatives, and computer systems can control processes which are too complex for hardwired solutions, or where the hardwired solution is uneconomic.     

Experiences applying formal approaches in the development of swarm-based space exploration systems

NASA is researching advanced technologies for future exploration missions using intelligent swarms of robotic vehicles. One of these missions is the Autonomous Nano-Technology Swarm (ANTS) mission that will explore the asteroid belt using 1,000 cooperative autonomous spacecraft. The emergent properties of intelligent swarms make it a potentially powerful concept, but at the same time more difficult to design and ensure that the proper behaviors will emerge. NASA is investigating formal methods and techniques for verification of such missions. The advantage of using formal methods is the ability to mathematically verify the behavior of a swarm, emergent or otherwise. Using the ANTS mission as a case study, we have evaluated multiple formal methods to determine their effectiveness in modeling and ensuring desired swarm behavior. This paper discusses the results of this evaluation and proposes an integrated formal method for ensuring correct behavior of future NASA intelligent swarms.     

Known-plaintext cryptanalysis of the Domingo-Ferrer algebraic privacy homomorphism scheme

We propose cryptanalysis of the First Domingo-Ferrer's algebraic privacy homomorphism where n=pq. We show that the scheme can be broken by (d+1) known plaintexts in O(d³log²n) time. Even when the modulus n is kept secret, it can be broken by 2(d+1) known plaintexts in O(d⁴logdn+d³log²n+?(m)) time with overwhelming probability.     

PalmHashing: a novel approach for cancelable biometrics

We propose a novel cancelable biometric approach, known as PalmHashing, to solve the non-revocable biometric issue. The proposed method hashes palmprint templates with a set of pseudo-random keys to obtain a unique code called palmhash. The palmhash code can be stored in portable devices such tokens and smartcards for verification. Multiple sets of palmhash codes can be maintained in multiple applications. Thus the privacy and security of the applications can be greatly enhanced. When compromised, revocation can also be achieved via direct replacement of a new set of palmhash code. In addition, PalmHashing offers several advantages over contemporary biometric approaches such as clear separation of the genuine-imposter populations and zero EER occurrences. In this paper, we outline the implementation details of this method and also highlight its potentials in security-critical applications.     

Relations between semantic security and anonymity in identity-based encryption

Semantic security and anonymity are the two main properties that an identity-based encryption scheme can satisfy. Such properties can be defined in either an adaptive or a selective scenario, which differ on the moment where the attacker chooses the identity/ies that are the target of the attack. There are well-known separations between selective and adaptive semantic security on the one hand, and between selective and adaptive anonymity on the other hand.In this paper we investigate the relations between these selective and adaptive notions, for identity-based encryption schemes enjoying at the same time some security and anonymity properties. On the negative side, we prove that there is a separation between selective and adaptive anonymity even for schemes which enjoy adaptive semantic security. On the positive side, we prove that selective semantic security and adaptive anonymity imply adaptive semantic security.     

Combinatorial lower bounds for secret sharing schemes

In a perfect secret sharing scheme, it holds that , where S denotes the secret and denotes the set of the share of user i. On the other hand, it is well known that if S is not uniformly distributed, where denotes the set of secrets. In this case, . Then, which is bigger, or We first prove that for any distribution on S by using a combinatorial argument. This is a more sharp lower bound on for not uniformly distributed S. Our proof makes it intuitively clear why must be so large. Next, we extend our technique to show that max_i for some access structure.     

连续傅里叶变换基础理论的高阶逻辑形式化

连续傅里叶变换(CFT)在数学和工程技术领域都有着广泛应用.利用高阶逻辑定理证明器HOL4,实现了对连续傅里叶变换定义及其常用运算性质的形式化,包括线性、频移、反转性、积分、时域一阶微分及高阶微分运算性质,为采用形式化方法分析相关系统奠定了基础.最后利用定理证明的方法对电阻电感电容(RLC)串联谐振电路的频率响应特性进行了验证,说明了CFT形式化的初步应用.