Search

When an applet is sent over the internet, Java Virtual Machine code is transmitted and remotely executed. Because untrusted code can be executed on the local computer running the web browser security problems may arise. We present a method to check illicit flows in Java bytecode, that exploits the type-level abstract interpretation of bytecode verification. We present an algorithm transforming a bytecode into another one that, when abstractly executed by the standard bytecode verifier, reveals illicit information flows. We show an example of application of the method.

The paper presents an approach for the specification and verification of the correctness of dependable system designs achieved by the application of fault tolerant techniques based on equivalence relations and model checking techniques. The behaviour of the system in absence of faults is formally specified and faults are assumed as random events which interfere with the system by modifying its behaviour. The fault tolerant technique is formalized by a context, which specifies how replicas of the system cooperate to deal with faults. The system design is proved to satisfy the correctness property under a given fault hypothesis, by proving the observational equivalence between the system design specification and the fault free system specification. Additionally, model checking of a temporal logic formula which gives an abstract notion of correct behaviour can be applied to verify the correctness of the design.