FRAMEWORK SYNTHESIS FOR SYMBOLIC EXECUTION OF EVENT-DRIVEN FRAMEWORKS

Symbolic execution is a powerful program analysis technique, but it is very challenging to apply to programs built using event-driven frameworks, such as Android. The main reason is that the framework code itself is too complex to symbolically execute. The standard solution is to manually create a framework model that is simpler and more amenable to symbolic execution. However, developing and maintaining such a model by hand is difficult and error-prone. We claim that we can leverage program synthesis to introduce a high-degree of automation to the process of framework modeling. To support this thesis, we present three pieces of work. First, we introduced SymDroid, a symbolic executor for Android. While Android apps are written in Java, they are compiled to Dalvik bytecode format. Instead of analyzing an app’s Java source, which may not be available, or decompiling from Dalvik back to Java, which requires significant engineering effort and introduces yet another source of potential bugs in an analysis, SymDroid works directly on Dalvik bytecode. Second, we introduced Pasket, a new system that takes a first step toward automatically generating Java framework models to support symbolic execution. Pasket takes as input the framework API and tutorial programs that exercise the framework. From these artifacts and Pasket's internal knowledge of design patterns, Pasket synthesizes an executable framework model by instantiating design patterns, such that the behavior of a synthesized model on the tutorial programs matches that of the original framework. Lastly, in order to scale program synthesis to framework models, we devised adaptive concretization, a novel program synthesis algorithm that combines the best of the two major synthesis strategies: symbolic search, i.e., using SAT or SMT solvers, and explicit search, e.g., stochastic enumeration of possible solutions. Adaptive concretization parallelizes multiple sub-synthesis problems by partially concretizing highly influential unknowns in the original synthesis problem. Thanks to adaptive concretization, Pasket can generate a large-scale model, e.g., thousands lines of code. In addition, we have used an Android model synthesized by Pasket and found that the model is sufficient to allow SymDroid to execute a range of apps.

The Effect of Package Geometry on Moisture Driven Degradation of Polymer Aluminum Capacitors

Polymer aluminum electrolytic capacitors were introduced to provide an alternative to liquid electrolytic capacitors. Polymer electrolytic capacitor electric parameters of capacitance and ESR are less temperature dependent than those of liquid aluminum electrolytic capacitors. Furthermore, the electrical conductivity of the polymer used in these capacitors (poly-3,4ethylenedioxithiophene) is orders of magnitude higher than the electrolytes used in liquid aluminum electrolytic capacitors, resulting in capacitors with much lower equivalent series resistance which are suitable for use in high ripple-current applications. The presence of the moisture-sensitive polymer PEDOT introduces concerns on the reliability of polymer aluminum capacitors in high humidity conditions. Highly accelerated stress testing (or HAST) (110ºC, 85% relative humidity) of polymer aluminum capacitors in which the parts were subjected to unbiased HAST conditions for 700 hours was done to understand the design factors that contribute to the susceptibility to degradation of a polymer aluminum electrolytic capacitor exposed to HAST conditions. A large scale study involving capacitors of different electrical ratings (2.5V – 16V, 100µF – 470 µF), mounting types (surface-mount and through-hole) and manufacturers (6 different manufacturers) was done to determine a relationship between package geometry and reliability in high temperature-humidity conditions. A Geometry-Based HAST test in which the part selection limited variations between capacitor samples to geometric differences only was done to analyze the effect of package geometry on humidity-driven degradation more closely. Raman spectroscopy, x-ray imaging, environmental scanning electron microscopy, and destructive analysis of the capacitors after HAST exposure was done to determine the failure mechanisms of polymer aluminum capacitors under high temperature-humidity conditions.