Biblio

There has been an ongoing trend toward collaborative software development using open and shared source code published in large software repositories on the Internet. While traditional source code analysis techniques perform well in single project contexts, new types of source code analysis techniques are ermerging, which focus on global source code analysis challenges. In this article, we discuss how the Semantic Web, can become an enabling technology to provide a standardized, formal, and semantic rich representations for modeling and analyzing large global source code corpora. Furthermore, inference services and other services provided by Semantic Web technologies can be used to support a variety of core source code analysis techniques, such as semantic code search, call graph construction, and clone detection. In this paper, we introduce SeCold, the first publicly available online linked data source code dataset for software engineering researchers and practitioners. Along with its dataset, SeCold also provides some Semantic Web enabled core services to support the analysis of Internet-scale source code repositories. We illustrated through several examples how this linked data combined with Semantic Web technologies can be harvested for different source code analysis tasks to support software trustworthiness. For the case studies, we combine both our linked-data set and Semantic Web enabled source code analysis services with knowledge extracted from StackOverflow, a crowdsourcing website. These case studies, we demonstrate that our approach is not only capable of crawling, processing, and scaling to traditional types of structured data (e.g., source code), but also supports emerging non-structured data sources, such as crowdsourced information (e.g., StackOverflow.com) to support a global source code analysis context.

Test input generators using symbolic and concolic execution must solve path conditions to systematically explore a program and generate high coverage tests. However, path conditions may contain complicated arithmetic constraints that are infeasible to solve: a solver may be unavailable, solving may be computationally intractable, or the constraints may be undecidable. Existing test generators either simplify such constraints with concrete values to make them decidable, or rely on strong but incomplete constraint solvers. Unfortunately, simplification yields coarse approximations whose solutions rarely satisfy the original constraint. Moreover, constraint solvers cannot handle calls to native library methods. We show how a simple combination of linear constraint solving and heuristic search can overcome these limitations. We call this technique Concolic Walk. On a corpus of 11 programs, an instance of our Concolic Walk algorithm using tabu search generates tests with two- to three-times higher coverage than simplification-based tools while being up to five-times as efficient. Furthermore, our algorithm improves the coverage of two state-of-the-art test generators by 21% and 32%. Other concolic and symbolic testing tools could integrate our algorithm to solve complex path conditions without having to sacrifice any of their own capabilities, leading to higher overall coverage.

Sharing data with client-side encryption requires key management. Selecting an appropriate key management protocol for a given scenario is hard, since the interdependency between scenario parameters and the resource consumption of a protocol is often only known for artificial, simplified scenarios. In this paper, we explore the resource consumption of systems that offer sharing of encrypted data within real-world scenarios, which are typically complex and determined by many parameters. For this purpose, we first collect empirical data that represents real-world scenarios by monitoring large-scale services within our organization. We then use this data to parameterize a resource consumption model that is based on the key graph generated by each key management protocol. The preliminary simulation runs we did so far indicate that this key-graph based model can be used to estimate the resource consumption of real-world systems for sharing encrypted data.

In this work, we analyze the stability properties of a recently proposed dynamical system that describes the evolution of the probability of infection in a network. We show that this model can be viewed as a concave game among the nodes. This characterization allows us to provide a simple condition, that can be checked in a distributed fashion, for stabilizing the origin. When the curing rates at the nodes are low, a residual infection stays within the network. Using properties of Hurwitz Mertzel matrices, we show that the residual epidemic state is locally exponentially stable. We also demonstrate that this state is globally asymptotically stable. Furthermore, we investigate the problem of stabilizing the network when the curing rates of a limited number of nodes can be controlled. In particular, we characterize the number of controllers required for a class of undirected graphs. Several simulations demonstrate our results.

We analyze the stability properties of a susceptible-infected-susceptible diffusion model over directed networks. Similar to the majority of infection spread dynamics, this model exhibits a threshold phenomenon. When the curing rates in the network are high, the all-healthy state is globally asymptotically stable (GAS). Otherwise, an endemic state arises and the entire network could become infected. Using notions from positive systems theory, we prove that the endemic state is GAS in strongly connected networks. When the graph is weakly connected, we provide conditions for the existence, uniqueness, and global asymptotic stability of weak and strong endemic states. Several simulations demonstrate our results.

This paper is concerned with mean-square stabilization of single-input Markovian jump linear systems (MJLSs) with logarithmically quantized state feedback. We introduce the concepts and provide explicit constructions of stabilizing mode-dependent logarithmic quantizers together with associated controllers, and a semi-convex way to determine the optimal (coarsest) stabilizing quantization density. An example application is presented as a special case of the developed framework, that of feedback stabilizing a linear time-invariant (LTI) system over a log-quantized erasure channel. A hardware implementation of this application on an inverted pendulum testbed is provided using a finite word-length approximation.

Web applications must ultimately command systems like web browsers and database engines using strings. Strings derived from improperly sanitized user input can thus be a vector for command injection attacks. In this paper, we introduce regular string types, which classify strings known statically to be in a specified regular language. These types come equipped with common operations like concatenation, substitution and coercion, so they can be used to implement, in a conventional manner, the portions of a web application or application framework that must directly construct com- mand strings. Simple type annotations at key interfaces can be used to statically verify that sanitization has been per- formed correctly without introducing redundant run-time checks. We specify this type system in a minimal typed lambda calculus, λRS.

To be practical, adopting a specialized type system like this should not require the adoption of a new programming language. Instead, we advocate for extensible type systems: new type system fragments like this should be implemented as libraries atop a mechanism that guarantees that they can be safely composed. We support this with two contribu- tions. First, we specify a translation from λRS to a language fragment containing only standard strings and regular ex- pressions. Second, taking Python as a language with these constructs, we implement the type system together with the translation as a library using atlang, an extensible static type system for Python being developed by the authors.

Application Programming Interfaces (APIs) often define object
protocols. Objects with protocols have a finite number of states and
in each state a different set of method calls is valid. Many researchers
have developed protocol verification tools because protocols are notoriously
difficult to follow correctly. However, recent research suggests that
a major challenge for API protocol programmers is effectively searching
the state space. Verification is an ineffective guide for this kind of
search. In this paper we instead propose Plaiddoc, which is like Javadoc
except it organizes methods by state instead of by class and it includes
explicit state transitions, state-based type specifications, and rich state
relationships. We compare Plaiddoc to a Javadoc control in a betweensubjects
laboratory experiment. We find that Plaiddoc participants complete
state search tasks in significantly less time and with significantly
fewer errors than Javadoc participants.

Software as a Service (SaaS) is the most prevalent service delivery mode for cloud systems. This paper surveys common security vulnerabilities and corresponding countermeasures for SaaS. It is primarily focused on the work published in the last five years. We observe current SaaS security trends and a lack of sufficiently broad and robust countermeasures in some of the SaaS security area such as Identity and Access management due to the growth of SaaS applications.
 

The emerging paradigm of cloud computing, e.g., Amazon Elastic Compute Cloud (EC2), promises a highly flexible yet robust environment for large-scale applications. Ideally, while multiple virtual machines (VM) share the same physical resources (e.g., CPUs, caches, DRAM, and I/O devices), each application should be allocated to an independently managed VM and isolated from one another. Unfortunately, the absence of physical isolation inevitably opens doors to a number of security threats. In this paper, we demonstrate in EC2 a new type of security vulnerability caused by competition between virtual I/O workloads-i.e., by leveraging the competition for shared resources, an adversary could intentionally slow down the execution of a targeted application in a VM that shares the same hardware. In particular, we focus on I/O resources such as hard-drive throughput and/or network bandwidth-which are critical for data-intensive applications. We design and implement Swiper, a framework which uses a carefully designed workload to incur significant delays on the targeted application and VM with minimum cost (i.e., resource consumption). We conduct a comprehensive set of experiments in EC2, which clearly demonstrates that Swiper is capable of significantly slowing down various server applications while consuming a small amount of resources.

The threshold secret sharing technique has been used extensively in cryptography. This technique is used for splitting secrets into shares and distributing the shares in a network to provide protection against attacks and to reduce the possibility of loss of information. In this paper, a new approach is introduced to enhance communication security among the nodes in a network based on the threshold secret sharing technique and traditional symmetric key management. The proposed scheme aims to enhance security of symmetric key distribution in a network. In the proposed scheme, key distribution is online which means key management is conducted whenever a message needs to be communicated. The basic idea is encrypting a message with a key (the secret) at the sender, then splitting the key into shares and sending the shares from different paths to the destination. Furthermore, a Pre-Distributed Shared Key scheme is utilized for more secure transmissions of the secret’s shares. The proposed scheme, with the exception of some offline management by the network controller, is distributed, i.e., the symmetric key setups and the determination of the communication paths is performed in the nodes. This approach enhances communication security among the nodes in a network that operates in hostile environments. The cost and security analyses of the proposed scheme are provided.

Decision makers need capabilities to quickly model and effectively assess consequences of actions and reactions in crisis de-escalation environments. The creation and what-if exercising of such models has traditionally had onerous resource requirements. This research demonstrates fast and viable ways to build such models in operational environments. Through social network extraction from texts, network analytics to identify key actors, and then simulation to assess alternative interventions, advisors can support practicing and execution of crisis de-escalation activities. We describe how we used this approach as part of a scenario-driven modeling effort. We demonstrate the strength of moving from data to models and the advantages of data-driven simulation, which allow for iterative refinement. We conclude with a discussion of the limitations of this approach and anticipated future work.

Self-protecting software systems are a class of autonomic systems capable of detecting and mitigating security threats at runtime. They are growing in importance, as the stovepipe static methods of securing software systems have been shown to be inadequate for the challenges posed by modern software systems. Self-protection, like other self-* properties, allows the system to adapt to the changing environment through autonomic means without much human intervention, and can thereby be responsive, agile, and cost effective. While existing research has made significant progress towards autonomic and adaptive security, gaps and challenges remain. This article presents a significant extension of our preliminary study in this area. In particular, unlike our preliminary study, here we have followed a systematic literature review process, which has broadened the scope of our study and strengthened the validity of our conclusions. By proposing and applying a comprehensive taxonomy to classify and characterize the state-of-the-art research in this area, we have identified key patterns, trends and challenges in the existing approaches, which reveals a number of opportunities that will shape the focus of future research efforts.

Concurrent programs are prone to various classes of difficult-to-detect faults, of which data races are particularly prevalent. Prior work has attempted to increase the cost-effectiveness of approaches for testing for data races by employing race detection techniques, but to date, no work has considered cost-effective approaches for re-testing for races as programs evolve. In this paper we present SimRT, an automated regression testing framework for use in detecting races introduced by code modifications. SimRT employs a regression test selection technique, focused on sets of program elements related to race detection, to reduce the number of test cases that must be run on a changed program to detect races that occur due to code modifications, and it employs a test case prioritization technique to improve the rate at which such races are detected. Our empirical study of SimRT reveals that it is more efficient and effective for revealing races than other approaches, and that its constituent test selection and prioritization components each contribute to its performance.

Much of the data researchers usually collect about users’ privacy and security behavior comes from short-term studies and focuses on specific, narrow activities. We present a design architecture for the Security Behavior Observatory (SBO), a client-server infrastructure designed to collect a wide array of data on user and computer behavior from a panel of hundreds of participants over several years. The SBO infrastructure had to be carefully designed to fulfill several requirements. First, the SBO must scale with the desired length, breadth, and depth of data collection. Second, we must take extraordinary care to ensure the security and privacy of the collected data, which will inevitably include intimate details about our participants’ behavior. Third, the SBO must serve our research interests, which will inevitably change over the course of the study, as collected data is analyzed, interpreted, and suggest further lines of inquiry. We describe in detail the SBO infrastructure, its secure data collection methods, the benefits of our design and implementation, as well as the hurdles and tradeoffs to consider when designing such a data collection system. 

Programming languages often include specialized syntax for common datatypes e.g. lists and some also build in support for specific specialized datatypes e.g. regular expressions, but user-defined types must use general-purpose syntax. Frustration with this causes developers to use strings, rather than structured data, with alarming frequency, leading to correctness, performance, security, and usability issues. Allowing library providers to modularly extend a language with new syntax could help address these issues. Unfortunately, prior mechanisms either limit expressiveness or are not safely composable: individually unambiguous extensions can still cause ambiguities when used together. We introduce type-specific languages TSLs: logic associated with a type that determines how the bodies of generic literals, able to contain arbitrary syntax, are parsed and elaborated, hygienically. The TSL for a type is invoked only when a literal appears where a term of that type is expected, guaranteeing non-interference. We give evidence supporting the applicability of this approach and formally specify it with a bidirectionally typed elaboration semantics for the Wyvern programming language.