Biblio

Proliferation of Android devices and apps has created a demand for applicable automated software testing techniques. Prior research has primarily focused on either unit or GUI testing of Android apps, but not their end-to-end system testing in a systematic manner. We present EvoDroid, an evolutionary approach for system testing of Android apps. EvoDroid overcomes a key shortcoming of using evolutionary techniques for system testing, i.e., the inability to pass on genetic makeup of good individuals in the search. To that end, EvoDroid combines two novel techniques: (1) an Android-specific program analysis technique that identifies the segments of the code amenable to be searched independently, and (2) an evolutionary algorithm that given information of such segments performs a step-wise search for test cases reaching deep into the code. Our experiments have corroborated EvoDroid’s ability to achieve significantly higher code coverage than existing Android testing tools.

Researchers interested in security often wish to introduce new primitives into a language. Extensible languages hold promise in such scenarios, but only if the extension mechanism is sufficiently safe and expressive. This paper describes several modifications to an extensible language motivated by end-to-end security concerns.

Access policies are hard to express in existing programming languages. However, their accurate expression is a prerequisite for many of today's applications. We propose a new language that uses classes, first-class relationships, and first-class states to express access policies in a more declarative and fine-grained way than existing solutions allow.

To help users create stronger text-based passwords, many web sites have deployed password meters that provide visual feedback on password strength. Although these meters are in wide use, their effects on the security and usability of passwords have not been well studied.

We present a 2,931-subject study of password creation in the presence of 14 password meters. We found that meters with a variety of visual appearances led users to create longer passwords. However, significant increases in resistance to a password-cracking algorithm were only achieved using meters that scored passwords stringently. These stringent meters also led participants to include more digits, symbols, and uppercase letters.

Password meters also affected the act of password creation. Participants who saw stringent meters spent longer creating their password and were more likely to change their password while entering it, yet they were also more likely to find the password meter annoying. However, the most stringent meter and those without visual bars caused participants to place less importance on satisfying the meter. Participants who saw more lenient meters tried to fill the meter and were averse to choosing passwords a meter deemed "bad" or "poor." Our findings can serve as guidelines for administrators seeking to nudge users towards stronger passwords.

The simplest and purest practical object-oriented language designs
today are seen in dynamically-typed languages, such as Smalltalk
and Self. Static types, however, have potential benefits for productivity,
security, and reasoning about programs. In this paper, we describe
the design of Wyvern, a statically typed, pure object-oriented
language that attempts to retain much of the simplicity and expressiveness
of these iconic designs.
Our goals lead us to combine pure object-oriented and functional
abstractions in a simple, typed setting. We present a foundational
object-based language that we believe to be as close as
one can get to simple typed lambda calculus while keeping objectorientation.
We show how this foundational language can be translated
to the typed lambda calculus via standard encodings. We then
define a simple extension to this language that introduces classes
and show that classes are no more than sugar for the foundational
object-based language. Our future intention is to demonstrate that
modules and other object-oriented features can be added to our language
as not more than such syntactical extensions while keeping
the object-oriented core as pure as possible.
The design of Wyvern closely follows both historical and modern
ideas about the essence of object-orientation, suggesting a new
way to think about a minimal, practical, typed core language for
objects.

Domain-specific languages improve ease-of-use, expressiveness and
verifiability, but defining and using different DSLs within a single
application remains difficult. We introduce an approach for embedded
DSLs where 1) whitespace delimits DSL-governed blocks, and
2) the parsing and type checking phases occur in tandem so that
the expected type of the block determines which domain-specific
parser governs that block. We argue that this approach occupies
a sweet spot, providing high expressiveness and ease-of-use while
maintaining safe composability. We introduce the design, provide
examples and describe an ongoing implementation of this strategy
in the Wyvern programming language. We also discuss how a more
conventional keyword-directed strategy for parsing of DSLs can
arise as a special case of this type-directed strategy.

Three years ago in this venue, Cook argued that in
their essence, objects are what Reynolds called procedural
data structures. His observation raises a natural
question: if procedural data structures are the essence
of objects, has this contributed to the empirical success
of objects, and if so, how?
This essay attempts to answer that question. After
reviewing Cook’s definition, I propose the term service
abstractions to capture the essential nature of objects.
This terminology emphasizes, following Kay, that
objects are not primarily about representing and manipulating
data, but are more about providing services
in support of higher-level goals. Using examples
taken from object-oriented frameworks, I illustrate the
unique design leverage that service abstractions provide:
the ability to define abstractions that can be extended,
and whose extensions are interoperable in a
first-class way. The essay argues that the form of interoperable
extension supported by service abstractions
is essential to modern software: many modern frameworks
and ecosystems could not have been built without
service abstractions. In this sense, the success of
objects was not a coincidence: it was an inevitable consequence
of their service abstraction nature.

Sandboxes impose a security policy, isolating applications
and their components from the rest of a system. While
many sandboxing techniques exist, state of the art sandboxes
generally perform their functions within the system
that is being defended. As a result, when the sandbox fails
or is bypassed, the security of the surrounding system can
no longer be assured. We experiment with the idea of innimbo
sandboxing, encapsulating untrusted computations
away from the system we are trying to protect. The idea
is to delegate computations that may be vulnerable or malicious
to virtual machine instances in a cloud computing
environment.
This may not reduce the possibility of an in-situ sandbox
compromise, but it could significantly reduce the consequences
should that possibility be realized. To achieve this
advantage, there are additional requirements, including: (1)
A regulated channel between the local and cloud environments
that supports interaction with the encapsulated application,
(2) Performance design that acceptably minimizes
latencies in excess of the in-situ baseline.
To test the feasibility of the idea, we built an in-nimbo
sandbox for Adobe Reader, an application that historically
has been subject to significant attacks. We undertook a
prototype deployment with PDF users in a large aerospace
firm. In addition to thwarting several examples of existing
PDF-based malware, we found that the added increment of
latency, perhaps surprisingly, does not overly impair the

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.

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 generalpurpose
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 noninterference.
We give evidence supporting the applicability of this approach and
formally specify it with a bidirectionally typed elaboration semantics for the
Wyvern programming language.

Static types may be used both by the language implementation and directly by the user as documentation. Though much existing work focuses primarily on the implications of static types on the semantics of programs, relatively little work considers the impact on usability that static types pro- vide. Though the omission of static type information may decrease program length and thereby improve readability, it may also decrease readability because users must then frequently derive type information manually while reading programs. As type inference becomes more popular in languages that are in widespread use, it is important to consider whether the adoption of type inference may impact productivity of developers.

Breaches of software security affect millions of people, and therefore it is crucial to strive for more secure software systems. However, the effect of programming language design on software security is not easily measured or studied. In the absence of scientific insight, opinions range from those that claim that programming language design has no effect on security of the system, to those that believe that programming language design is the only way to provide “high-assurance software.” In this paper, we discuss how programming language design can impact software security by looking at a specific example: the Wyvern programming language. We report on how the design of the Wyvern programming language leverages security principles, together with hypotheses about how usability impacts security, in order to prevent command injection attacks. Furthermore, we discuss what security principles we considered in Wyvern’s design.

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.

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 de- tecting races introduced by code modifications. SIMRT employs a regression test selection technique, focused on sets of program ele- ments 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 prioritiza- tion 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 con- stituent test selection and prioritization components each contribute to its performance.

State estimation plays a critically important role in ensuring the secure and reliable operation of the electric grid. Recent works have shown that the state estimation process is vulnerable to stealthy attacks where an adversary can alter certain measurements to corrupt the solution of the process, but evade the existing bad data detection algorithms and remain invisible to the system operator. Since the state estimation result is used to compute optimal power flow and perform contingency analysis, incorrect estimation can undermine economic and secure system operation. However, an adversary needs sufficient resources as well as necessary knowledge to achieve a desired attack outcome. The knowledge that is required to launch an attack mainly includes the measurements considered in state estimation, the connectivity among the buses, and the power line admittances. Uncertainty in information limits the potential attack space for an attacker. This advantage of uncertainty enables us to apply moving target defense (MTD) strategies for developing a proactive defense mechanism for state estimation.

In this paper, we propose an MTD mechanism for securing state estimation, which has several characteristics: (i) increase the knowledge uncertainty for attackers, (ii) reduce the window of attack opportunity, and (iii) increase the attack cost. In this mechanism, we apply controlled randomization on the power grid system properties, mainly on the set of measurements that are considered in state estimation, and the topology, especially the line admittances. We thoroughly analyze the performance of the proposed mechanism on the standard IEEE 14- and 30-bus test systems.

Phishing is a social engineering tactic that targets internet users in an attempt to trick them into divulging personal information. When opening an email, users are faced with the decision of determining if an email is legitimate or an attempt at phishing. Although software has been developed to assist the user, studies have shown they are not foolproof, leaving the user vulnerable. Multiple training programs have been developed to educate users in their efforts to make informed decisions; however, training that conveys the real world consequences of phishing or training that increases a user’s fear level have not been developed. Conveying real world consequences of a situation and increasing a user’s fear level have been proven to enhance the effects of training in other fields. Ninety-six participants were recruited and randomly assigned to training programs with phishing consequences, training programs designed to increase fear, or a control group. Preliminary results indicate that training helped users identify phishing emails; however, little difference was seen among the three groups. Future analysis will include a factor analysis of personality and individual differences that influence training efficacy.

We propose Cupid, a language for specifying commitments that supports their information-centric aspects, and offers crucial benefits.  One, Cupid is first-order, enabling a systematic treatment of commitment instances.  Two, Cupid supports features needed for real-world scenarios such as deadlines, nested commitments, and complex event expressions for capturing the lifecycle of commitment instances.  Three, Cupid maps to relational database queries and thus provides a set-based semantics for retrieving commitment instances in states such as being violated,discharged, and so on.  We prove that Cupid queries are safe.  Four,to aid commitment modelers, we propose the notion of well-identified commitments, and finitely violable and finitely expirable commitments.  We give syntactic restrictions for obtaining such commitments.