Critical vulnerabilities continue to be discovered in the boot process of Android smartphones used around the world. The entire device's security is compromised if boot security is compromised, so any weakness presents undue risk to users. Vulnerabilities persist, in part, because independent security analysts lack access and appropriate tools. In response to this gap, we implemented a procedure for emulating the early phase of the Android boot process. This work demonstrated feasibility and utility of emulation in this space. By using HALucinator, we derived execution context and data flow, as well as incorporated peripheral hardware behavior. While smartphones with shared processors have substantial code overlap regardless of vendor, generational changes can have a significant impact. By applying our approach to older and modern devices, we learned interesting characteristics about the system. Such capabilities introduce new levels of introspection and operation understanding not previously available to mobile researchers.
Many real-world engineering and science problems can be mapped to Boolean satisfiability problems (SAT). CDCL SAT solvers are among the most efficient solvers. Previous work showed that instances derived from a particular problem class exhibit a unique underlying structure which impacts the effectiveness of a solver's variable selection scheme. Thus, customizing the variable scoring heuristic of a solver to a particular problem class can significantly enhance the solver's performance; however, manually performing such customization is very labor intensive. This paper presents a system for automating the design of variable scoring heuristics for CDCL solvers, making it feasible to tailor solvers to arbitrary problem classes. Experimental results are provided demonstrating that this system, which evolves variable scoring heuristics using an asynchronous parallel hyper-heuristics approach employing genetic programming, has the potential to create more efficient solvers for particular problem classes.
Understanding the data structures employed by a program is important for reverse engineering activities and can improve the results of automated software analysis techniques. In a compiled binary, access to data structure fields and array indices defined in the source program are replaced by raw pointer arithmetic. We present a representation for capturing the essential details of how a program accesses memory regions, which we call a Memory Access Graph (MAG), and a static analysis for automatically extracting this information from a program binary. The static analysis to extract the MAGs from the program is straightforward and does not require sophisticated integer or pointer analysis. The MAGs are readily understood by reverse engineers; they are generally able to perceive the data structure definition corresponding to a MAG. We briefly discuss automatic extraction of structure definitions outlining some of the difficulties in doing so.