Using Contour Marking Bytecode Verification Algorithm on the Java Card

Java bytecode verification could not be well performed in the smart card due to the resource usage especially in the resource-constrained devices. Currently, on the card there are several bytecode verifications which exist kinds of problems, in order to be better and be better adapt to the environment, such as a smart card platform, raised using the contour subroutine labeled bytecode verification algorithm on a card. First, through the analysis of existing card byte code verification algorithm to determine the imperfections and difficulties in the judgment and the verification of subroutine, and then propose a method for marking the subroutine in the place of the jump to it. Thus not only get the program structure and enhance the effectiveness and efficiency of the validation. The feasibility of the method is demonstrated by simulating typical examples verification.

Secure distributed programming with value-dependent types

Distributed applications are difficult to program reliably and securely. Dependently typed functional languages promise to prevent broad classes of errors and vulnerabilities, and to enable program verification to proceed side-by-side with development. However, as recursion, effects, and rich libraries are added, using types to reason about programs, specifications, and proofs becomes challenging. We present F*, a full-fledged design and implementation of a new dependently typed language for secure distributed programming. Our language provides arbitrary recursion while maintaining a logically consistent core; it enables modular reasoning about state and other effects using affine types; and it supports proofs of refinement properties using a mixture of cryptographic evidence and logical proof terms. The key mechanism is a new kind system that tracks several sub-languages within F* and controls their interaction. F* subsumes two previous languages, F7 and Fine. We prove type soundness (with proofs mechanized in Coq) and logical consistency for F*. We have implemented a compiler that translates F* to .NET bytecode, based on a prototype for Fine. F* provides access to libraries for concurrency, networking, cryptography, and interoperability with C#, F#, and the other .NET languages. The compiler produces verifiable binaries with 60% code size overhead for proofs and types, as much as a 45x improvement over the Fine compiler, while still enabling efficient bytecode verification. We have programmed and verified nearly 50,000 lines of F* including new schemes for multi-party sessions; a zero-knowledge privacy-preserving payment protocol; a provenance-aware curated database; a suite of web-browser extensions verified for authorization properties; a cloud-hosted multi-tier web application with a verified reference monitor; the core F* typechecker itself; and programs translated to F* from other languages such as F7 and JavaScript.