James Wilcox

2papers

2 Papers

CRJun 2, 2021
Phoenix: A Formally Verified Regenerating Vault

Uri Kirstein, Shelly Grossman, Michael Mirkin et al.

An attacker that gains access to a cryptocurrency user's private keys can perform any operation in her stead. Due to the decentralized nature of most cryptocurrencies, no entity can revert those operations. This is a central challenge for decentralized systems, illustrated by numerous high-profile heists. Vault contracts reduce this risk by introducing artificial delay on operations, allowing abortion by the contract owner during the delay. However, the theft of a key still renders the vault unusable and puts funds at risk. We introduce Phoenix, a novel contract architecture that allows the user to restore its security properties after key loss. Phoenix takes advantage of users' ability to store keys in easily-available but less secure storage (tier-two) as well as more secure storage that is harder to access (tier-one). Unlike previous solutions, the user can restore Phoenix security after the theft of tier-two keys and does not lose funds despite losing keys in either tier. Phoenix also introduces a mechanism to reduce the damage an attacker can cause in case of a tier-one compromise. We formally specify Phoenix's required behavior and provide a prototype implementation of Phoenix as an Ethereum contract. Since such an implementation is highly sensitive and vulnerable to subtle bugs, we apply a formal verification tool to prove specific code properties and identify faults. We highlight a bug identified by the tool that could be exploited by an attacker to compromise Phoenix. After fixing the bug, the tool proved the low-level executable code's correctness.

MED-PHSep 29, 2018
Pulsed Schlieren Imaging of Ultrasonic Haptics and Levitation using Phased Arrays

Michele Iodice, William Frier, James Wilcox et al.

Ultrasonic acoustic fields have recently been used to generate haptic effects on the human skin as well as to levitate small sub-wavelength size particles. Schlieren imaging and background-oriented schlieren techniques can be used for acoustic wave pattern and beam shape visualization. These techniques exploit variations in the refractive index of a propagation medium by applying refractive optics or cross-correlation algorithms of photographs of illuminated background patterns. Here both background-oriented and traditional schlieren systems are used to visualize the regions of the acoustic power involved in creating dynamic haptic sensations and dynamic levitation traps. We demonstrate for the first time the application of back-ground-oriented schlieren for imaging ultrasonic fields in air. We detail our imaging apparatus and present improved algorithms used to visualize these phenomena that we have produced using multiple phased arrays. Moreover, to improve imaging, we leverage an electronically controlled, high-output LED which is pulsed in synchrony with the ultrasonic carrier frequency.