JAWS (Java Applets With Safety) is an ACSys project using theorem-proving technology to analyse safety and security properties of Java applets.
Gary McGraw and Edward Felten in their recent book Java Security: Hostile Applets, Holes, and Antidotes provide an excellent summary of the current state of Java Security. As they put it:
"All of these features of Java are certainly exciting. However, Java's fantastic potential is mitigated by very serious security concerns. Security is always an issue when computers are networked together. Realistically speaking, there is no such thing as a computer system that is 100% secure (Cheswick and Bellovin, 1994). Because of this fact, users of networked computers must weigh the benefits of being connected to the world against the risks that they incur by connecting in the first place."
"One of the key selling points of Java is its use as a "cross-platform" language for creating executable content on the Internet. Simply by using a web browser, a web surfer can take advantage of Java's cross-platform capability. Of course, the activity of locally running code created and compiled somewhere else has important security implications."
"The same technology that allows Java applets to liven up once-static web pages also allows unscrupulous applet designers to invade an unsuspecting Java user's machine."
The so-called "Orange Book" (U.S. Department of Defense Trusted Computer System Evaluation Criteria, December l985) requires that all systems (C1 and above) have a Trusted Computing Base (TCB) which
"...shall maintain a domain for its own execution that protects it from external interference or tampering (e.g., by modification of its code or data structures)."
The Java Virtual Machine fails to satisfy this requirement, since security is provided by several components of the run-time system (byte-code verifier, class loader, security manager) which have in the past not adequately protected themselves from modification (witness a number of bugs discovered by Felten and the Princeton Safe Internet Programming team). Indeed, the Internet community's experience with large, monolithic, security-critical programs, such as sendmail (still a security threat as of version 8.8.4) has not been encouraging. The timing of the Java security bugs (in Netscape Navigator and Microsoft Internet Explorer) reported by the Princeton Safe Internet Programming team and others fits a logarithmic distribution, shown in the diagram below. This implies that there will always be one more bug, even though bugs will become rarer with time.
At higher levels of assurance (B1 and above), the Orange Book requires that an
"...informal or formal model of the security policy supported by the TCB shall be maintained over the life cycle of the ADP system and demonstrated to be consistent with its axioms."
As McGraw and Felten point out, Java has no formal security policy, which makes analysis of java security difficult.
The ITSEC (Information Technology Security Evaluation Criteria, the European version of the Orange Book) at the E3 level (corresponding to B1) states:
"Any programming languages used for implementation shall be well-defined, e.g. as in an ISO standard. Any implementation dependent options of the programming language shall be documented."
"The definition of the programming languages shall define unambiguously the meaning of all statements used in the source code."
Another difficulty with analysing Java security is that neither Java source code nor Java byte code have a well-defined formal semantics, although it is clear that the semantics of the source code and byte code do not match completely.
The JAWS project is developing answers to some of these questions, and thereby providing a way of delivering the benefits of applets safely and securely.