Recent advances in program synthesis convinced us that it was the right time to transform the process of porting an operating system into a program synthesis problem. We set out to synthesize the needed machine dependent code for an existing operating system. This undertaking proved far more challenging than we anticipated. We summarize our experience and lessons learned and propose next steps in realizing such an undertaking.
This technical report describes two of the domain-specific languages used in the Aquarium kernel code synthesis project. It presents the language cores in terms of abstract syntax. Cassiopea is a machine description language for describing the semantics of processor instruction sets. Alewife is a specification language that can be used to write machine-independent specifications for assembly-level instruction blocks. An Alewife specification can be used to verify and synthesize code for any machine described in Cassiopea, given a machine-specific translation for abstractions used in the specification. This article does not include an introduction to either the Aquarium system or the use of the languages. In addition to this version of the article being a draft, the Aquarium project and the languages are work in progress. This article cannot currently be considered either final or complete.
Smartphones have been widely used with a vast array of sensitive and private information stored on these devices.
To secure such information from being leaked, user authentication schemes are necessary. Current password/pattern-based user authentication schemes are vulnerable to shoulder surfing attacks and smudge attacks. In contrast, stroke/gait-based schemes are secure but inconvenient for users to input. In this paper, we propose ShakeIn, a handy user authentication scheme for secure unlocking of a smartphone by simply shaking the phone. With embedded motion sensors, ShakeIn can effectively capture the unique and reliable biometrical features of users about how they shake. In this way, even if an attacker sees a user shaking his/her phone, the attacker can hardly reproduce the same behavior. Furthermore, by allowing users to customize the way they shake the phone, ShakeIn endows users with the maximum operation flexibility. We implement ShakeIn and conduct both intensive trace-driven simulations and real experiments on 20 volunteers with about 530,555 shaking samples collected over multiple months. The results show that ShakeIn achieves an average equal error rate of 1.2 percent with a small number of shakes using only 35 training samples even in the presence of shoulder-surfing attacks.