Search

Java Bytecode Verification was so far mostly approached from a correctness perspective. Security vulnerabilities have been found repeatedly and were corrected shortly thereafter. However, correctness is not the only potential point of failure in the verifier idea. In this paper we construct Java code, which is correct, but requires an excessive amount of time to prove safety. In contrast to previous flaws in the bytecode verifier, the enabling property for this exploit lies in the verification algorithm itself and not in the implementation and is thus not easily fixable. We explain how this architectural weakness could be exploited for denial-of-service attacks on JVM-based services and devices.

The safety of the Java Virtual Machine is founded on bytecode verification. Although verification complexity appears to roughly correlate with program size in. the average case, its worst-case behavior is quadratic. This can be exploited for denial-of-service attacks using relatively short programs (applets or agents) specifically crafted to keep the receiving virtual machine's verifier busy for an inordinate amount of time. Instead of the existing, quadratic-complexity verification algorithm, which needs to decide the validity of any given bytecode program, we present a linear-complexity alternative that merely ensures that no unsafe program is ever passed on to the virtual machine. Hence, in certain cases, our algorithm will modify an unsafe bytecode program to make it safe, a process that we call 'proofing". Proofing does not change the semantics of programs that would have passed the original bytecode verifier. For programs that would have failed verification, our algorithm will, in linear time, either reject them, or transform them into programs (of unspecified semantics) that are guaranteed to be safe. Our method also solves a long-standing problem, in which for certain perfectly legal Java source programs the bytecodes produced by Java compilers are erroneously rejected by existing verifiers.

We are in the midst of a paradigm shift toward component-oriented software development, and significant progress has been made in understanding and harnessing this new paradigm. Somewhat strangely then, the new paradigm does not currently extend all the way down to how the components themselves are constructed. While we have composition architectures and languages that describe how systems are put together out of such atomic program parts, the parts themselves are still constructed based on a previous paradigm, object-oriented programming. We argue that this represents a mismatch that is holding back compositional software design: many of the assumptions that underly object-oriented systems simply do not apply in the open and dynamic contexts of component software environments. What, then, would a programming language look like that supported component-oriented programming at the smallest granularity? Our project to develop such a language, Lagoona, tries to provide an answer to this question. This paper motivates the new key concepts behind Lagoona and briefly describes their realization (using Lagoona itself as the implementation language) in the context of Microsoft's .NET environment.

One of Java's most fundamental core concepts is dynamic class loading. While being very practical in the general purpose domain, the runtime cost of dynamic class loading poses a significant challenge for the deployment of Java applications in embedded systems. In this paper we describe a mechanism called static class loading which allows to perform the resource-intensive class loading process at compile-time while preserving the full class-loading semantics as defined in the Java specification. This eliminates the need for a byte-code interpreter and allows to translate all Java code to native code ahead-of-time, saving valuable resources on the target platform.

A combined approach of chromatic immunoprecipitation and parallel sequencing of genomic DNA was utilized to identify a gene, FAM161A which was shown to carry a homozygous nonsense mutation (p.Arg229X) in patients form the original retinitis pigmentosa 28 (RP28) pedigrees. The data obtained indicated that the RP28-associated arRP is attributed to the null mutations in FAM161A.

Java Virtual Machines (JVMs) traditionally perform bytecode verification by way of an iterative dataflow analysis. Bytecode verification is necessary to ensure type safety because temporary variables in the JVM are not statically typed. We present an alternative verification mechanism that transforms JVM bytecode into Static Single Assignment Form (SSA) and thereby propagates definitions directly to uses. Type checking at control flow merge points can then be performed in a single pass. Our prototype implementation of the new algorithm is faster than the standard JVM bytecode verifier. It has the additional benefit of generating SSA as a side effect, which may be immediately useful for a subsequent dynamic compilation stage. Categories and Subject Descriptors: D.2.4 [Software Engineering]: Software/Program Verification--Validation; D.3.4 [Programming Languages]: Processors--Compilers General Terms: Algorithms, Design, Experimentation, Languages, Performance, Security, Verification Additional Key Words and Phrases: Java bytecode verification, static single assignment form, dataflow analysis

The heterozygous de novo point mutations, a missense mutation (p.R217C) and a nonsense mutation (p.R197X), in the HCCS gene is identified in two female patients, from two families, with microphthalmia with linear skin defects syndrome. It is demonstrated that both mutant proteins (R217C and A197-268) are unable to complement a Saccharomyces cerevisiae mutant deficient for the HCCS orthologue Cyc3p, in contrast to wild type HCCS.