Search

Security of programming languages, particularly programming languages used for network applications, is a major issue at this time. Despite the best efforts of language designers and implementers, serious security vulnerabilities continue to be discovered at an alarming rate. Thus, development of analysis tools that can be used to uncover insecure or malicious code is an important area of research. This thesis focuses on the use of the lightweight formal method tool Alloy to perform static analysis on binary code, Byte-compiled languages that run on virtual machines are of particular interest because of their relatively small instruction sets, and also because they are well represented on the Internet. This thesis describes a static analysis methodology in which desired security properties of a language are expressed as constraints in Alloy, while the actual bytes being analyzed are expressed as Alloy model initializers. The combination of these two components yields a complete Alloy model in which any model counterexample represents a constraint violation, and hence a security vulnerability. The general method of expressing security requirements as constraints is studied, and results are presented for Java bytecodes running on the Java Virtual Machine, as well as for Adobe Flash SWF files containing ActionScript bytecodes running on the Action Script Virtual Machine. It is demonstrated that many examples of malware are detected by this technique. In addition, analysis of benign software is shown to not produce any counterexamples. This represents a significant departure from standard methods based on signatures or anomaly detection.