Ian Blumenfeld

Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, the more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, model validation, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a… Show more

Verification of hardware-based cryptographic accelerators connects a low-level RTL implementation to the abstract algorithm itself; generally, the more optimized for performance an accelerator is, the more challenging its verification. This paper introduces a verification methodology, model validation, that uses a formalized high-level synthesis language (FHLS) as an intermediary between algorithm specification and hardware implementation. The foundation of our approach to model validation is a mechanized denotational semantics for the ReWire HLS language. Model validation proves the faithfulness of FHLS models to the RTL implementation and we summarize a model validation case study for a suite of pipelined Barrett multipliers. Show less

We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3).
SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a pre-shared password to authenticate each other and establish a session key. SRP aims to resist… Show more

We analyze the Secure Remote Password (SRP) protocol for structural weaknesses using the Cryptographic Protocol Shapes Analyzer (CPSA) in the first formal analysis of SRP (specifically, Version 3).
SRP is a widely deployed Password Authenticated Key Exchange (PAKE) protocol used in 1Password, iCloud Keychain, and other products. As with many PAKE protocols, two participants use knowledge of a pre-shared password to authenticate each other and establish a session key. SRP aims to resist dictionary attacks, not store plaintext-equivalent passwords on the server, avoid patent infringement, and avoid export controls by not using encryption. Formal analysis of SRP is challenging in part because existing tools provide no simple way to reason about its use of the mathematical expression v+gbmodq.
Modeling v+gb as encryption, we complete an exhaustive study of all possible execution sequences of SRP. Ignoring possible algebraic attacks, this analysis detects no major structural weakness, and in particular no leakage of any secrets. We do uncover one notable weakness of SRP, which follows from its design constraints. It is possible for a malicious server to fake an authentication session with a client, without the client's participation. This action might facilitate an escalation of privilege attack, if the client has higher privileges than does the server. We conceived of this attack before we used CPSA and confirmed it by generating corresponding execution shapes using CPSA. Show less

This talk describes CherryPie, a program analysis-based approach to accelerate the discovery of logic bombs in software. Detecting logic bombs during system certification requires discov-ering undesirable functionality that is explicitly designed to avoid discovery. A high-impact logic bomb must be carefully hidden to avoid accidental triggering. CherryPie exploits this requirement to identify potential logic bombs by recognizing code within a software appli-cation that are unlikely to be… Show more

This talk describes CherryPie, a program analysis-based approach to accelerate the discovery of logic bombs in software. Detecting logic bombs during system certification requires discov-ering undesirable functionality that is explicitly designed to avoid discovery. A high-impact logic bomb must be carefully hidden to avoid accidental triggering. CherryPie exploits this requirement to identify potential logic bombs by recognizing code within a software appli-cation that are unlikely to be exercised during test or normal operations. These results can be used to prioritize program regions for manual analysis or targeted test vector generation. The core algorithms of CherryPie are (a) a multi-colored taint analysis used to identify program locations that depend on a variety of program state elements, and (b) symbolic execution with SMT model estimation to prioritize the identified locations based on the fraction of program state space satisfying the location's path condition. Initial testing of CherryPie against a logic bomb inserted in the Angband text adventure game demonstrated the potential of the approach by eliminating almost two thirds of program blocks as unlikely to contain logic bombs based on taint analysis and rating the actual block implementing the trigger as three orders of magnitude more likely to be a logic bomb than other blocks. These early results suggest that CherryPie may be able to greatly accelerate the costly manual process of evaluating critical software for the presence logic bombs. Show less

Proportional Integral Derivative (PID) controllers are ubiquitous in cyber- physical systems, from industrial control to drones. Their simplicity and well-understood dynamics make them perfect candidates for safety critical applications. However, simplicity of design is inevitably compromised to ad- dress departures of the real-world systems from the idealized linear dynamics. For example, low-pass filtering may be added to reduce noise in the feedback signal, gain scheduling may be added to… Show more

Proportional Integral Derivative (PID) controllers are ubiquitous in cyber- physical systems, from industrial control to drones. Their simplicity and well-understood dynamics make them perfect candidates for safety critical applications. However, simplicity of design is inevitably compromised to ad- dress departures of the real-world systems from the idealized linear dynamics. For example, low-pass filtering may be added to reduce noise in the feedback signal, gain scheduling may be added to account for non-linearity in response, and output clamping may be added to constrain the control signal to an ac- ceptable range. As the complexity of the controller design grows, ensuring correct and safe operation of the system becomes a real challenge.

We demonstrate an approach based on hybrid systems analysis and formal methods that allows theorems about safety and correctness of a PID con- troller to be extended to the source code level implementation. This approach is explored through an application to the heading controller of an Unmanned Underwater Vehicle (UUV). We show how the hydrodynamic model of the UUV can be combined with the mathematical specification of the PID con- troller logic to verify roll angle safety using the KeYmaera X hybrid systems theorem prover. This is a mainly mathematical endeavor, where the main challenge is adapting well-known control theory results based on Lyapunov function theory to KeYmaera X's differential dynamic logic formalism. The resulting proofs establish the safety of the controller at the specification level.

We then use the type constraint mechanisms and proof capabilities of SPARK / GNATprove to formally verify that the source-level SPARK implementa- tion of the controller logic satisfies the assumptions of the KeYmaera X specification proofs. In particular, we are using SPARK contracts to verify that floating point calculations preserve the desired PID recurrences Show less

Over the last year, the Johns Hopkins Applied Physics Laboratory has been pursuing research in verification of cyber-physical industrial control systems. We have successfully applied the hybrid systems theorem prover KeyMaera-X to the analysis of a model of a shipboard chilled water system. The physics of this model is governed by a system of ordinary differential equations that are more complex than those used in previous KeyMaera-X proofs. With assistance from the KeyMaera-X team at Carnegie… Show more

Over the last year, the Johns Hopkins Applied Physics Laboratory has been pursuing research in verification of cyber-physical industrial control systems. We have successfully applied the hybrid systems theorem prover KeyMaera-X to the analysis of a model of a shipboard chilled water system. The physics of this model is governed by a system of ordinary differential equations that are more complex than those used in previous KeyMaera-X proofs. With assistance from the KeyMaera-X team at Carnegie Mellon University, we were able to demonstrate a safety property that a load in the system would not overheat under a reasonable set of assumptions. Our model included a simple control logic and a set of realistic differential equations that describe the cooling of a load in the presence of chilled water. Following the completion of these proofs, we demonstrated the sharpness of the bounds in the safety property using dReach, a bounded reachability analysis tool for hybrid systems. This work shows a promising approach for formal analysis of real-world cyber-physical industrial control systems, and we are working to expand this work to other problems in this domain. Show less

In order to perform in-depth malware analysis, reverse engineers must first overcome advanced packing methods employed by malware authors. We investigated using an SMT solver for undoing some of the code obfuscation used by a particular packer. In this note we describe the issues, our approach, and preliminary results.