Abstract
Programs contain bugs. Finding program bugs is important, especially in situations where safety and security of a program is required. This thesis proposes a number of analysis methods for enforcing the absence of such bugs. In the first part of the thesis the Java Modeling Language (JML) is the main object of study. The expressiveness of JML is shown by specifying the behavior a number of semantically complex Java program fragments. Program verifications tools, such as the LOOP verification framework and ESC/Java, are used to formally prove the correctness of these specifications. We also show how JML can be used to ensure a safe and secure control flow for a complete Java card applet and how JML can be used to express secure information flow in Java programs. Secure information flow, or confidentiality, is central in the second part of the thesis. Several program verification techniques are introduced that enforce security properties, specifically confidentiality. The idea is that we want a (provably sound) analysis technique that enforces a secure information flow policy for a program. Such a policy typically specifies what information -contained in the program- is secret and what information is publicly available. Non-interference is the technical notion used to prove confidentiality for programs. Informally, a program is deemed non-interfering if its low level (public) output values are completely independent of high level (secret) input variables of a program. Several forms of non-interference have been studied in the literature. The most common (and also the weakest) form is termination-insensitive non-interference. In this case non-interference is only guaranteed if the program terminates normally, if the program hangs or terminates abruptly (via an exception) non-interference is not necessarily assured. In contrast, termination-sensitive non-interference ensures the non-interference property for all termination modes. Still stronger forms of non-interference also take covert channels, such as the timing behavior of a program, into account. Which leads to notions such as time-sensitive termination-sensitive non-interference. Abstract interpretation, interactive theorem proving, program transformation and specification generation techniques are used to enforce each of the different notions of non-interference discussed above.
