Modern computer security research spans multiple levels of abstractions, dealing with topics ranging from provably secure cryptographic building blocks to large and socially important distributed systems. In this talk I describe three projects that represent different points along this continuum. (1) I describe my research improving the security of the popular Secure Shell (SSH) protocol against a privacy attack that I discovered. I then describe how I prove the security of my fixes using the principles of modern reduction-based provable security. My research here is both formal and systems-oriented; the latter means that when I create my formal models and definitions, I pay close attention to the constraints and goals of the existing SSH protocol. (2) I describe a method for remotely distinguishing two physical devices even if those two devices have the same hardware and software configuration. My technique exploits a new information leakage channel in the TCP protocol: by analyzing the stream of TCP packets from a device, it is in some cases possible to infer information about the transmitting device’s clock skew. My approach has applications to computer forensics, detecting virtualization technologies, counting the number of devices behind a NAT, and de-anonymizing anonymized network traces. (3) I describe serious attacks against a deployed electronic voting machine, namely a version of the Diebold AccuVote-TS electronic voting machine. I then describe some social and technical implications of my results as well as future directions.