Lecture notes by Lynette I. Millett
For example, in C, bad (invalid) pointers can cause programs (and, in some cases, even the operating system) to crash. One approach to solving this problem is to disallow pointer arithmetic. However, to completely solve this problem, we must also disallow 'free' as well, as otherwise deallocated objects might be access through pointers to them. If neither pointer arithmetic nor 'free' statements are allowed in a language, then it is not possible to access an invalid pointer. (The disadvantage is that without 'free', it is now necessary to do garbage collection.)
We see, therefore, that restricting a language can be useful for security purposes. (In fact, a language like "skip" is very secure.) Java, however, is much more expressive than "skip", so we examine it instead. Some general facts about Java:
If we would like to run this program, the Java program is compiled into a simple assembly-like language that runs on the Java Virtual Machine (JVM).class Queue { private int[] els; private int pos; public int getFromFront() { . . . } public void addToBack(int i) { pos := pos + 1; els[pos] = i; } public boolean empty() { . . . } }
where this refers to the instance of the Queue object that is running. Consider the top of the stack after each of these statements. After the first statement, the Queue object is on top of the stack. After the second, an integer is on top. Executing push 1 means that now two integers are on top of the second. Finally, iadd pops the two integers off the top and pushes the result.Top of Stack push this Queue get int Queue.pos int push 1 int, int iadd int
Note that there are other languages that compile to VMs as we have described. They are not as successful, primarily because Java runs more efficiently and with more safety. How is this achieved? The difference is at what stages Java does certain things. At runtime, the JVM does some checks for safety (such as divide by 0 and array bounds checking.) Many other similar languages also do type checking here (e.g., checking to be sure that an integer add operation was really operating on two integers.) Java does not do this at runtime, instead, a verifier runs at load time to ensure that, for example, iadd is called only when two integers are on top of that stack.
What does this verifier have to do? For every JVM instruction, if the instruction uses a global reference (such as Queue.pos), then it should make sure that it is correct. (For instance, only Queue can reference Queue.pos, since pos is private.) Global references are checked by name. The local state is also checked. That is, the stack and registers are checked to be sure that the types are correct. This is what we are interested in. If we can do this sort of type checking, then we have made progress towards verifying safety properties of the language. To enforce type-correctness, the verifier looks through the code, method-by-method, and makes sure that the register and stack are in proper states.
The most important property verified is the Gosling property (after one of Java's creators.) This property says that the stack and registers must always look the same whenever a JVM instruction is executed. In other words, the stack must be the same size, registers must be in the same defined/undefined state, and types must be the same. The Gosling property should hold whatever the control flow. Consider the following code segment.
At goto L1, there should be an integer on the stack. Suppose that the statement push this was just before the goto statement. Then, the verifier should reject this program. Otherwise, the JVM would add an object to an integer. The following code segment is acceptable, however.Top of Stack push this Queue get int Queue.pos int L1: push 1 int, int iadd int . . . goto L1
In this case, there is an integer on the stack before the goto executes, which ensures that there are two ints on the stack when we do iadd.Top of Stack push this Queue get int Queue.pos int L1: push 1 int, int iadd int goto L1
The Gosling property is easy to reason about and enforce, however, it is quite restrictive. There is safe code that violates the Gosling property. Consider the following pseudo-code:
Here, before the second if, reg1 is either an integer or a Newspaper object. The Gosling property says that the stack and registers should always look the same, regardless of control flow. In this example, they don't, and even though this code fragment makes sense and is safe, the verifier would reject it. In fact, the Gosling property is even too simple for the Java language. Consider the constructif input == 0 then reg1 = int 7; else reg1 = Newspaper n; skip <--- unsafe state if input == 0 then return reg1 else return reg1.NumPages
whose semantics is: always do X, even if one of the pi fails. X may execute after any one of the pi, but there's nothing that says the registers and stack are in the same state after each pi. One way to solve this is to have the verifier make sure that X does not use whatever is varying from one pi to the next. This requires a more complicated analysis, making the verifier much more complicated than it would be if this construct were not in the language. This is rather unfortunate, as this construct is not one of the most commonly used.try {p1; p2; p3} finally { X }
What do we mean by safety? We insist that only legitimate accesses to objects are allowed. We also insist that only meaningful operations be allowed on objects. Succinctly: restrict who can access what, and how they can access it. This should sound familiar, as it is precisely what the access control matrix from models. We can formulate safety using an access control matrix. In fact, the object oriented nature of Java facilitates this. Operations and objects are explicit and we know what operations are meaningful from the class definition. If we include classes in the ACM, then we see some nice properties. For instance, file access can be excluded just be denying access to the FILE class. Further, code might still store/retrieve FILE objects as generic objects (java.lang.Object) even though it couldn't use them as FILEs. Consider the Java ACM for the Queue object discussed previously.
We need a more powerful rights annotation system. We say that the Queue object has three types of rights: direct, add and get. In this situation, subjects that access els and pos require the direct access. Calling the method getFromFront requires the get right, calling addToBack requires the add right, and empty doesn't require any rights. In this manner, we can specify explicitly which rights are needed. Then, we could give code exactly the rights they need, and even statically check that they satisfy their rights requirements, as in the following example where one Queue is appended to another.
One problem with this type of scheme is that it can be difficult to handle dynamic rights.Append(Queue[add] dest, Queue[get] source) { while(!src.empty()) { dest.addToBack(src.getFromFront()); } }
It's important to note that most security issues discussed above have little to do with with the Java language itself, but rather with the verifier that works on JVM byte code. This yield two advantages: any language that can be compiled to Java byte code can be verified and even handwritten byte code (which is likely to be used for attacks) can be checked.
The verifier ensures that the code is type-correct. What exactly does type-correctness mean? In general, this means that the code does not violate interfaces. That is, integer addition should operate on integers, printf should take a string as its first argument, and so on. The original motivation for type-correctness was not security, but rather software engineering: Ensuring type-correctness reduces the chance of programmer error and allows implementations to change without changing interfaces.
Aside from the fact that reducing programmer error can help with respect to security issues, how is type-correctness relevant to security? It turns out that the properties enforced by type-correctness overlap with the properties we want from a secure program.
How does Java itself use type-correctness to achieve better security? Java's original popularity was due to applets (not to do with its security properties.) The security for applets (an example is diagrammed below)
This policy is enforced by the SecurityManager (SM). The SM is hooked to code/thread at load time. If the code is an applet, then the appletSM is attached; if the code is local, then a nullSM is attached. The SM is queried by a method call when services are used. For instance, if an applet tries to read a file x, then its SM is queried: is this allowed?
Consider an example where there are three domains: editor, encryption and filesystem. The editor makes use of the encryption domain to load and save encrypted files from the filesystem. Now suppose the editor would like to save a file. It makes a call to encryption. Encryption calls the file system which calls checkPermission(Files) to ensure that the calling domians have the Files permission. This scenario is depicted below:
In Java 1.2 the policy is that checkPermission(Files) does not succeed unless all domains crossed by the calling thread (here the three domains figured) have the Files permission. This is actually implemented in the JVM by tracing back up the call stack and examining the domains crossed.
The mechanism described above automatically attenuates the Permissions of a thread to be the intersection of the Permissions of all crossed domains. But, in addition to attenuation, it is often necessary to amplify rights. E.g., the file system may need to log activity, using the Log permission, no matter who calls it.
Consider the following scenario: A Login domain, having permissions for the screen and keyboard, makes use of a PasswdCheck domain to check the entered passwords. The PasswdCheck domain, having rights to cryptography and the password file, encrypts passwords and checks the result against the password file, using the filesystem domain. The following figure shows this scenario without amplification, and when checkPermission(PasswdFile) is called, not all crossed domains have the PasswdFile permission, and the check therefore fails.
try { beginPrivileged(); security_critical_code } finally { endPrivileged(); }
This new Java 1.2 security mechanism is much better than the previous Java Sandbox. For Example, the Permissions mechanism can be used by applications such as databases, not just by system services such as the Filesystem. On the other hand, there is still no audit facility. Moreover, amplification of beginPrivileged amplifies to all permissions for that domain, there is no way to do beginPrivileged(Files). Finally, this mechanism is too static. It is not possible to do things that rely on the history of the application, e.g., this policy does not allow enforcement of "no network send after read."