Theses and Dissertations from UMD

Permanent URI for this communityhttp://hdl.handle.net/1903/2

New submissions to the thesis/dissertation collections are added automatically as they are received from the Graduate School. Currently, the Graduate School deposits all theses and dissertations from a given semester after the official graduation date. This means that there may be up to a 4 month delay in the appearance of a give thesis/dissertation in DRUM

More information is available at Theses and Dissertations at University of Maryland Libraries.

Browse

Subject: search.filters.subject.computer science

Search Results

Now showing 1 - 3 of 3
  • Thumbnail Image
    Item
    Design for Just-In-Time: Resource Design for Self-Teaching Computer Science and Online Learning
    (2020) Lindeman, Carrie Lucille; Weintrop, David; Library & Information Services; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    The goal of this study is to investigate how just-in-time resources may support self-teaching for adult computer science learners who are new to coding. For people learning computer science on their own, just-in-time resources can be essential for solving problems. A popular online resource that computer scientists of all experience levels rely on is Stack Overflow, a forum that has a question and answer format. Resources like Stack Overflow can help new programmers problem-solve their code without consulting a teacher or professor. However, these resources may be creating barriers in the learning experience that should prepare them for future computer science education. By observing learners using just-in-time resources and interviewing learners about their habits, this thesis provides guidance on potential design suggestions for better supporting users’ future learning. Understanding how just-in-time materials currently support self-teaching for adult novice computer science learners will provide the foundation for these designs.
  • Thumbnail Image
    Item
    Mechanizing Abstract Interpretation
    (2017) Darais, David Charles; Van Horn, David; Computer Science; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    It is important when developing software to verify the absence of undesirable behavior such as crashes, bugs and security vulnerabilities. Some settings require high assurance in verification results, e.g., for embedded software in automobiles or airplanes. To achieve high assurance in these verification results, formal methods are used to automatically construct or check proofs of their correctness. However, achieving high assurance for program analysis results is challenging, and current methods are ill suited for both complex critical domains and mainstream use. To verify the correctness of software we consider program analyzers---automated tools which detect software defects---and to achieve high assurance in verification results we consider mechanized verification---a rigorous process for establishing the correctness of program analyzers via computer-checked proofs. The key challenges to designing verified program analyzers are: (1) achieving an analyzer design for a given programming language and correctness property; (2) achieving an implementation for the design; and (3) achieving a mechanized verification that the implementation is correct w.r.t. the design. The state of the art in (1) and (2) is to use abstract interpretation: a guiding mathematical framework for systematically constructing analyzers directly from programming language semantics. However, achieving (3) in the presence of abstract interpretation has remained an open problem since the late 1990's. Furthermore, even the state-of-the art which achieves (3) in the absence of abstract interpretation suffers from the inability to be reused in the presence of new analyzer designs or programming language features. First, we solve the open problem which has prevented the combination of abstract interpretation (and in particular, calculational abstract interpretation) with mechanized verification, which advances the state of the art in designing, implementing, and verifying analyzers for critical software. We do this through a new mathematical framework Constructive Galois Connections which supports synthesizing specifications for program analyzers, calculating implementations from these induced specifications, and is amenable to mechanized verification. Finally, we introduce reusable components for implementing analyzers for a wide range of designs and semantics. We do this though two new frameworks Galois Transformers and Definitional Abstract Interpreters. These frameworks tightly couple analyzer design decisions, implementation fragments, and verification properties into compositional components which are (target) programming-language independent and amenable to mechanized verification. Variations in the analysis design are then recovered by simply re-assembling the combination of components. Using this framework, sophisticated program analyzers can be assembled by non-experts, and the result are guaranteed to be verified by construction.
  • Thumbnail Image
    Item
    EMPIRICAL STUDIES BASED ON HONEYPOTS FOR CHARACTERIZING ATTACKERS BEHAVIOR
    (2015) Sobesto, Bertrand; Cukier, Michel; Reliability Engineering; Digital Repository at the University of Maryland; University of Maryland (College Park, Md.)
    The cybersecurity community has made substantial efforts to understand and mitigate security flaws in information systems. Oftentimes when a compromise is discovered, it is difficult to identify the actions performed by an attacker. In this study, we explore the compromise phase, i.e., when an attacker exploits the host he/she gained access to using a vulnerability exposed by an information system. More specifically, we look at the main actions performed during the compromise and the factors deterring the attackers from exploiting the compromised systems. Because of the lack of security datasets on compromised systems, we need to deploy systems to more adequately study attackers and the different techniques they employ to compromise computer. Security researchers employ target computers, called honeypots, that are not used by normal or authorized users. In this study we first describe the distributed honeypot network architecture deployed at the University of Maryland and the different honeypot-based experiments enabling the data collection required to conduct the studies on attackers' behavior. In a first experiment we explore the attackers' skill levels and the purpose of the malicious software installed on the honeypots. We determined the relative skill levels of the attackers and classified the different software installed. We then focused on the crimes committed by the attackers, i.e., the attacks launched from the honeypots by the attackers. We defined the different computer crimes observed (e.g., brute-force attacks and denial of service attacks) and their characteristics (whether they were coordinated and/or destructive). We looked at the impact of computer resources restrictions on the crimes and then, at the deterrent effect of warning and surveillance. Lastly, we used different metrics related to the attack sessions to investigate the impact of surveillance on the attackers based on their country of origin. During attacks, we found that attackers mainly installed IRC-based bot tools and sometimes shared their honeypot access. From the analysis on crimes, it appears that deterrence does not work; we showed attackers seem to favor certain computer resources. Lastly, we observed that the presence of surveillance had no significant impact on the attack sessions, however surveillance altered the behavior originating from a few countries.