Security analysis of bytecode interpreters using Alloy

• Main Author: Reynolds, Mark Clifford
• Language: en_US
• Published: Boston University 2018
• Subjects: Programming languages; Security analysis; Digital security
• Online Access: https://hdl.handle.net/2144/32048

Thesis (Ph.D.)--Boston University === PLEASE NOTE: Boston University Libraries did not receive an Authorization To Manage form for this thesis or dissertation. It is therefore not openly accessible, though it may be available by request. If you are the author or principal advisor of this work and would like to request open access for it, please contact us at [e-mail]. Thank you. === 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. === 2031-01-02