Search

This paper focuses on scalable static analysis techniques for finding information leaks in Android apps. Finding such leaks scalably is challenging because Android apps have on average over 100 invocations of sensitive APIs, yielding a massive multi-source taint analysis problem. We present the design of STAR, a context-sensitive and flow-sensitive multi-source taint analysis aimed at tackling this problem. STAR incorporates two main ideas to achieve high performance and scalability. The first is a novel summarization technique we refer to as symbolic summarization, which is crucial for the analysis to scale well with the number of source APIs. The second is a combination of techniques aimed at efficient propagation of abstract states both within and across method boundaries. Our experiments over a dataset composed of 400,000 apps show that the proposed techniques improve performance over an IFDS-style analysis by a factor of 30 on average, and by up to four orders of magnitude on large apps.

With the increased number of small electronics and demand for their energy source, renewable energy sources have received much attention. Above all, a triboelectric nanogenerator (TENG) based on the combination of contact electrification and electrostatic induction has been researched as a method of converting mechanical energy into electricity. In order to increase the electrical output of TENGs with raising the surface charge density, a lot of researchers have focused on the fabrication methods to employ micro-/nano-structures onto a contact surface of the TENG, but have been facing several issues regarding the degradation of the output performance from the iterative operation process. Hence, it is highly required to introduce an approach to enhancing the performance of TENG, while minimally degrading the output power during the long-term operation. In this paper, an air-gap embedded TENG (AE-TENG), which contains a microstructure on the non-contact surface by means of a sandpaper, is proposed. These small air-gaps between the spin-coated polydimethylsiloxane and the non-contact surface can significantly boost the total surface charge density of the dielectric layer. Thus, the electrical output performance of the AE-TENG is enhanced without any surface engineering on the contact surface. Furthermore, the effect of the air-gap induced surface charges on the electric potential is systematically analyzed by not only experimentally electrical outputs, but theoretical and computational modeling based on the V-Q-x relationship and simulation software tool. This air-gap induced triboelectric effect opens a new perspective of the development of electrical outputs by providing a structural/theoretical understanding for TENGs.

With the increased number of small electronics and demand for their energy source, renewable energy sources have received much attention. Above all, a triboelectric nanogenerator (TENG) based on the combination of contact electrification and electrostatic induction has been researched as a method of converting mechanical energy into electricity. In order to increase the electrical output of TENGs with raising the surface charge density, a lot of researchers have focused on the fabrication methods to employ micro-/nano-structures onto a contact surface of the TENG, but have been facing several issues regarding the degradation of the output performance from the iterative operation process. Hence, it is highly required to introduce an approach to enhancing the performance of TENG, while minimally degrading the output power during the long-term operation. In this paper, an air-gap embedded TENG (AE-TENG), which contains a microstructure on the non-contact surface by means of a sandpaper, is proposed. These small air-gaps between the spin-coated polydimethylsiloxane and the non-contact surface can significantly boost the total surface charge density of the dielectric layer. Thus, the electrical output performance of the AE-TENG is enhanced without any surface engineering on the contact surface. Furthermore, the effect of the air-gap induced surface charges on the electric potential is systematically analyzed by not only experimentally electrical outputs, but theoretical and computational modeling based on the V–Q–x relationship and simulation software tool. This air-gap induced triboelectric effect opens a new perspective of the development of electrical outputs by providing a structural/theoretical understanding for TENGs.

In recent years, several automated GUI testing techniques for Android apps have been proposed. These tools have been shown to be effective in achieving good test coverage and in finding bugs without human intervention. Being automated, these tools typically run for a long time (say, for several hours), either until they saturate test coverage or until a testing time budget expires. Thus, these automated tools are not good at generating concise regression test suites that could be used for testing in incremental development of the apps and in regression testing. We propose a heuristic technique that helps create a small regression test suite for an Android app from a large test suite generated by an automated Android GUI testing tool. The key insight behind our technique is that if we can identify and remove some common forms of redundancies introduced by existing automated GUI testing tools, then we can drastically lower the time required to minimize a GUI test suite. We have implemented our algorithm in a prototype tool called DetReduce. We applied DetReduce to several Android apps and found that DetReduce reduces a test-suite by an average factor of 16.9× in size and 14.7× in running time. We also found that for a test suite generated by running SwiftHand and a randomized test generation algorithm for 8 hours, DetReduce minimizes the test suite in an average of 14.6 hours.

Dynamic symbolic execution (DSE) has been proposed to effectively generate test inputs for real-world programs. Unfortunately, DSE techniques do not scale well for large realistic programs, because often the number of feasible execution paths of a program increases exponentially with the increase in the length of an execution path. In this paper, we propose MultiSE, a new technique for merging states incrementally during symbolic execution, without using auxiliary variables. The key idea of MultiSE is based on an alternative representation of the state, where we map each variable, including the program counter, to a set of guarded symbolic expressions called a value summary. MultiSE has several advantages over conventional DSE and conventional state merging techniques: value summaries enable sharing of symbolic expressions and path constraints along multiple paths and thus avoid redundant execution. MultiSE does not introduce auxiliary symbolic variables, which enables it to 1) make progress even when merging values not supported by the constraint solver, 2) avoid expensive constraint solver calls when resolving function calls and jumps, and 3) carry out most operations concretely. Moreover, MultiSE updates value summaries incrementally at every assignment instruction, which makes it unnecessary to identify the join points and to keep track of variables to merge at join points. We have implemented MultiSE for JavaScript programs in a publicly available open-source tool. Our evaluation of MultiSE on several programs shows that 1) value summaries are an eective technique to take advantage of the sharing of value along multiple execution path, that 2) MultiSE can run significantly faster than traditional dynamic symbolic execution and, 3) MultiSE saves a substantial number of state merges compared to conventional state-merging techniques.

We propose a static type system for a significant subset of JavaScript, dubbed SJS, with the goal of ensuring that objects have a statically known layout at the allocation time, which in turn can enable an ahead-of-time (AOT) compiler to generate efficient code.The main technical challenge we address is to ensure fixed object layout, while supporting popular language features such as objects with prototype inheritance, structural subtyping, and method updates, with the additional constraint that SJS programs can run on any available standard JavaScript engine, with no deviation from JavaScript’s standard operational semantics. The core difficulty arises from the way standard JavaScript semantics implements object attribute update with prototype-based inheritance. To our knowledge, combining a fixed object layout property with prototype inheritance and subtyping has not been achieved previously.

Smartphones and tablets with rich graphical user interfaces (GUI) are becoming increasingly popular. Hundreds of thousands of specialized applications, called apps, are available for such mobile platforms. Manual testing is the most popular technique for testing graphical user interfaces of such apps. Manual testing is often tedious and error-prone. In this paper, we propose an automated technique, called Swift-Hand, for generating sequences of test inputs for Android apps. The technique uses machine learning to learn a model of the app during testing, uses the learned model to generate user inputs that visit unexplored states of the app, and uses the execution of the app on the generated inputs to refine the model. A key feature of the testing algorithm is that it avoids restarting the app, which is a significantly more expensive operation than executing the app on a sequence of inputs. An important insight behind our testing algorithm is that we do not need to learn a precise model of an app, which is often computationally intensive, if our goal is to simply guide test execution into unexplored parts of the state space. We have implemented our testing algorithm in a publicly available tool for Android apps written in Java. Our experimental results show that we can achieve significantly better coverage than traditional random testing and L*-based testing in a given time budget. Our algorithm also reaches peak coverage faster than both random and L*-based testing.

Smartphones and tablets with rich graphical user interfaces are becoming increasingly popular. Hundreds of thousands of specialized applications, called apps, are available for such mobile platforms. Manual testing is the most popular technique for testing graphical user interfaces of such apps. Manual testing is often tedious and error-prone.In this talk I will describe a new automated technique, called SwiftHand [2], for generating sequences of test inputs for Android apps. The technique gradually learns a behavioral model of the target app during testing, uses the learned model to generate user in- puts that visit unexplored states of the app, and uses the execution of the app on the generated inputs to refine the model. The technique is inspired by Angluin's L*[1] active learning algorithm and is designed to minimize the cost of learning. We have implemented our testing algorithm in a publicly available tool for Android apps written in Java. Our experimental results show that we can achieve significantly better coverage than traditional random testing and L* -based testing in a given time budget. Our algorithm also reaches peak coverage faster than both random and L*-based testing.The second half of the talk will be focused on challenges to implements this technique for the Android mobile platform. This work is a collaboration with Prof. George Necula and Prof. Koushik Sen.

Generic programming (GP) is an increasingly important trend in programming languages. Well-known GP mechanisms, such as type classes and the C++0x concepts proposal, usually combine two features: 1) a special type of interfaces; and 2) implicit instantiation of implementations of those interfaces. Scala implicits are a GP language mechanism, inspired by type classes, that break with the tradition of coupling implicit instantiation with a special type of interface. Instead, implicits provide only implicit instantiation, which is generalized to work for any types . This turns out to be quite powerful and useful to address many limitations that show up in other GP mechanisms. This paper synthesizes the key ideas of implicits formally in a minimal and general core calculus called the implicit calculus (λ⇒), and it shows how to build source languages supporting implicit instantiation on top of it. A novelty of the calculus is its support for partial resolution and higher-order rules (a feature that has been proposed before, but was never formalized or implemented). Ultimately, the implicit calculus provides a formal model of implicits, which can be used by language designers to study and inform implementations of similar mechanisms in their own languages.

Due to copyright restrictions, the access to the full text of this article is only available via subscription. Static analysis of multi-staged programs is challenging because thebasic assumption of conventional static analysis no longer holds: the program text itself is no longer a fixed static entity, but rather a dynamically constructed value. This article presents a semanticpreserving translation of multi-staged call-by-value programs into unstaged programs and a static analysis framework based on this translation. The translation is semantic-preserving in that every small-step reduction of a multi-staged program is simulated by the evaluation of its unstaged version. Thanks to this translation we can analyze multi-staged programs with existing static analysis techniques that have been developed for conventional unstaged programs: we first apply the unstaging translation, then we apply conventional static analysis to the unstaged version, and finally we cast the analysis results back in terms of the original staged program. Our translation handles staging constructs that have beenevolved to be useful in practice (typified in Lisp’s quasi quotation): open code as values, unrestricted operations on references and intentional variable-capturing substitutions. This article omits references for which we refer the reader to our companion technical report. Engineering Research Center of Excellence Program of Korea Ministry of Education, Science and Technology(MEST) ; National Research Foundation of Korea(NRF)

As information technologies have developed, the digital library is making the library undergo a changing paradigm of its role to create, organize, and distribute information resources. Digital libraries have created and promoted innovative information services with digitization of resources. The development of digital libraries has been attracting the attention of many countries and South Korea is no exception. This article provides an overview of recent developments in digital libraries in South Korea. To build the digital library, various innovative projects are currently in progress involving a range of different libraries and institutions. This article also discusses information policies, standards, and technical issues in South Korea in recent years. Until now, the various projects involving digital collections and digital libraries in South Korea have been carried out with very little coordination. If a more coordinated and coherent approach to building digital libraries is to succeed in South Korea, all libraries and institutions will need to work closely together to establish the appropriate framework for cooperation.