This thesis is concerned with the quantitative assessment of security in software. More specifically, it tackles the problem of efficient computation of channel capacity, the maximum amount of confidential information leaked by software, measured in Shannon entropy or R²nyi's min-entropy. Most approaches to computing channel capacity are either efficient and return only (possibly very loose) upper bounds, or alternatively are inefficient but precise; few target realistic programs. In this thesis, we present a novel approach to the problem by reducing it to a model counting problem on first-order logic, which we name Model Counting Modulo Theories or #SMT for brevity. For quantitative security, our contribution is twofold. First, on the theoretical side we establish the connections between measuring confidentiality leaks and fundamental verification algorithms like Symbolic Execution, SMT solvers and DPLL. Second, exploiting these connections, we develop novel #SMT-based techniques to compute channel capacity, which achieve both accuracy and efficiency. These techniques are scalable to real-world programs, and illustrative case studies include C programs from Linux kernel, a Java program from a European project and anonymity protocols. For formal verification, our contribution is also twofold. First, we introduce and study a new research problem, namely #SMT, which has other potential applications beyond computing channel capacity, such as returning multiple-counterexamples for Bounded Model Checking or automated test generation. Second, we propose an alternative approach for Bounded Model Checking using classical Symbolic Execution, which can be parallelised to leverage modern multi-core and distributed architecture. For software engineering, our first contribution is to demonstrate the correspondence between the algorithm of Symbolic Execution and the DPLL(T ) algorithm used in state-of-the-art SMT solvers. This correspondence could be leveraged to improve Symbolic Execution for automated test generation. Finally, we show the relation between computing channel capacity and reliability analysis in software.

With the rapid development of the internet, copying a digital document is so easy and economically affordable that digital piracy is rampant. As a result, software protection has become a vital issue in current computer industry and a hot research topic. Software watermarking and obfuscation are techniques to protect software from unauthorized access, modification, and tampering. While software watermarking tries to insert a secret message called software watermark into the software program as evidence of ownership, software obfuscation translates software into a semantically- equivalent one that is hard for attackers to analyze. In this thesis, firstly, we present a survey of software watermarking and obfuscation. Then we formalize two impor- tant concepts in software watermarking: extraction and recognition and we use a concrete software watermarking algorithm to illustrate issues in these two concepts. We develop a technique called the homomorphic functions through residue numbers to obfuscate variables and data structures in software programs. Lastly, we explore the complexity issues in software watermarking and obfuscation.

With the rapid development of the internet, copying a digital document is so easy and economically affordable that digital piracy is rampant. As a result, software protection has become a vital issue in current computer industry and a hot research topic. Software watermarking and obfuscation are techniques to protect software from unauthorized access, modification, and tampering. While software watermarking tries to insert a secret message called software watermark into the software program as evidence of ownership, software obfuscation translates software into a semantically- equivalent one that is hard for attackers to analyze. In this thesis, firstly, we present a survey of software watermarking and obfuscation. Then we formalize two impor- tant concepts in software watermarking: extraction and recognition and we use a concrete software watermarking algorithm to illustrate issues in these two concepts. We develop a technique called the homomorphic functions through residue numbers to obfuscate variables and data structures in software programs. Lastly, we explore the complexity issues in software watermarking and obfuscation.

With the rapid development of the internet, copying a digital document is so easy and economically affordable that digital piracy is rampant. As a result, software protection has become a vital issue in current computer industry and a hot research topic. Software watermarking and obfuscation are techniques to protect software from unauthorized access, modification, and tampering. While software watermarking tries to insert a secret message called software watermark into the software program as evidence of ownership, software obfuscation translates software into a semantically- equivalent one that is hard for attackers to analyze. In this thesis, firstly, we present a survey of software watermarking and obfuscation. Then we formalize two impor- tant concepts in software watermarking: extraction and recognition and we use a concrete software watermarking algorithm to illustrate issues in these two concepts. We develop a technique called the homomorphic functions through residue numbers to obfuscate variables and data structures in software programs. Lastly, we explore the complexity issues in software watermarking and obfuscation.

With the rapid development of the internet, copying a digital document is so easy and economically affordable that digital piracy is rampant. As a result, software protection has become a vital issue in current computer industry and a hot research topic. Software watermarking and obfuscation are techniques to protect software from unauthorized access, modification, and tampering. While software watermarking tries to insert a secret message called software watermark into the software program as evidence of ownership, software obfuscation translates software into a semantically- equivalent one that is hard for attackers to analyze. In this thesis, firstly, we present a survey of software watermarking and obfuscation. Then we formalize two impor- tant concepts in software watermarking: extraction and recognition and we use a concrete software watermarking algorithm to illustrate issues in these two concepts. We develop a technique called the homomorphic functions through residue numbers to obfuscate variables and data structures in software programs. Lastly, we explore the complexity issues in software watermarking and obfuscation.

Security defects or vulnerabilities are inescapable in software development. Thus, it is always better to address security issues during the software development phases, rather than developing patches after the security threats are already in place. In line with this, a number of secure software development approaches have been proposed so far to address the security issues during the development processes. However, most of these approaches lack specific process improvement activities. The practice of taking adequate corrective measures at the earliest possible time by learning from the past mistakes is absent in case of such security-aware iterative software development processes. As one might imagine, software security defect data provide an invaluable source of information for a software development team. This thesis aims at investigating existing security defect classification schemes and providing a structured security-specific defect classification and analysis methodology. Our methodology which we build on top of the Orthogonal Defect Classification (ODC) scheme, is customized to generate in-process feedback by analyzing security defect data. More specifically, we perform a detailed analysis on the classified security defect data and obtain in-process feedback using which the next version of software can be more secure and reliable. We experiment our methodology on the Mozilla Firefox and Chrome security defect repositories using six consecutive versions and milestones, respectively. We find that the in-process feedback generated by applying this methodology can help take corrective actions as early as possible in iterative secure software development processes. Finally, we study the correlations between software security defect types and the phases of software development life-cycle to understand development improvement by complementing the previous ODC scheme. / Thesis (Master, Computing) -- Queen's University, 2012-10-30 15:47:34.47

In recent years, the number of exploits targeting software applications has increased dramatically. These exploits have caused substantial economic damages. Ensuring that software applications are not vulnerable to the exploits has, therefore, become a critical requirement. The last line of defense is to test before hand if a software application is vulnerable to exploits. One can accomplish this by testing for the presence of vulnerabilities. This dissertation presents a framework for deriving verification and validation (V&V) strategies to assess the security of a software application by testing it for the presence of vulnerabilities. This framework can be used to assess the security of any software application that executes above the level of the operating system. It affords a novel approach, which consists of testing if the software application permits violation of constraints imposed by computer system resources or assumptions made about the usage of these resources. A vulnerability exists if a constraint or an assumption can be violated. Distinctively different from other approaches found in the literature, this approach simplifies the process of assessing the security of a software application. The framework is composed of three components: (1) a taxonomy of vulnerabilities, which is an informative classification of vulnerabilities, where vulnerabilities are expressed in the form of violable constraints and assumptions; (2) an object model, which is a collection of potentially vulnerable process objects that can be present in a software application; and (3) a V&V strategies component, which combines information from the taxonomy and the object model; and provides approaches for testing software applications for the presence of vulnerabilities. This dissertation also presents a step-by-step process for using the framework to assess software security. / Ph. D.

<p>This thesis has investigated what different tools for static code analysis, with anemphasis on security, there exist and which of these that possibly could be used in a project at Ericsson AB in Linköping in which a HIGA (Home IMS Gateway) is constructed. The HIGA is a residential gateway that opens up for the possibility to extend an operator’s Internet Multimedia Subsystem (IMS) all the way to the user’s home and thereby let the end user connect his/her non compliant IMS devices, such as a media server, to an IMS network.</p><p>Static analysis is the process of examining the source code of a program and in that way test a program for various weaknesses without having to actually execute it (compared to dynamic analysis such as testing).</p><p>As a complement to the regular testing, that today is being performed in the HIGA project, four different static analysis tools were evaluated to find out which one was best suited for use in the HIGA project. Two of them were open source tools and two were commercial.</p><p>All of the tools were evaluated in five different areas: documentation, installation & integration procedure, usability, performance and types of bugs found. Furthermore all of the tools were later on used to perform testing of two modules of the HIGA.</p><p>The evaluation showed many differences between the tools in all areas and not surprisingly the two open source tools turned out to be far less mature than the commercial ones. The tools that were best suited for use in the HIGA project were Fortify SCA and Flawfinder.</p><p>As far as the evaluation of the HIGA code is concerned some different bugs which could have jeopardized security and availability of the services provided by it were found.</p>

abstract: Data protection has long been a point of contention and a vastly researched field. With the advent of technology and advances in Internet technologies, securing data has become much more challenging these days. Cloud services have become very popular. Given the ease of access and availability of the systems, it is not easy to not use cloud to store data. This however, pose a significant risk to data security as more of your data is available to a third party. Given the easy transmission and almost infinite storage of data, securing one's sensitive information has become a major challenge. Cloud service providers may not be trusted completely with your data. It is not very uncommon to snoop over the data for finding interesting patterns to generate ad revenue or divulge your information to a third party, e.g. government and law enforcing agencies. For enterprises who use cloud service, it pose a risk for their intellectual property and business secrets. With more and more employees using cloud for their day to day work, business now face a risk of losing or leaking out information. In this thesis, I have focused on ways to protect data and information over cloud- a third party not authorized to use your data, all this while still utilizing cloud services for transfer and availability of data. This research proposes an alternative to an on-premise secure infrastructure giving exibility to user for protecting the data and control over it. The project uses cryptography to protect data and create a secure architecture for secret key migration in order to decrypt the data securely for the intended recipient. It utilizes Intel's technology which gives it an added advantage over other existing solutions. / Dissertation/Thesis / Masters Thesis Computer Science 2016

Understanding the communications between programs can help software security engineers understand the behaviour of a system and detect vulnerabilities in a system. Assembly-level execution traces are used for this purpose for two reasons: 1) lack of source code of the running programs, and 2) assembly-level execution traces provide the most accurate run-time behaviour information. In this thesis, I present a communication analysis approach using such execution traces. I first model the message based communication in the context of trace analysis. Then I develop a method and the necessary algorithms to identify communications from a dual trace which consist of two assembly level execution traces. A prototype is developed for communication analysis. Finally, I conducted two experiments for communication analysis of interacting programs. These two experiments show the usefulness of the designed communication analysis approach, the developed algorithms and the implemented prototype. / Graduate / 2019-05-11