Lead Institution: Johns Hopkins University

Project Leader: Avi Rubin

Research Progress

• Abstract
  The goal of this project was to remove the errors inherent in the development of cryptographic schemes by automating code generation and formal verification. We built three systems, AutoBatch, AutoGroup, and CloudSource

  • AutoBatch automates the design of batch verification algorithms from high-level descriptions of signature schemes. Since our initial publication last year, we have further improved and evaluated the tool against different crypto libraries to show generality. Also, we added a new technique for further optimization gains in a few of our test cases. Finally, we prepared and released the source code to the research community.
  • CloudSource automates the outsourcing of decryption computations between an untrusted but computationally-powerful cloud server and a trusted, lightweight client. We have developed a prototype tool that builds on AutoBatch techniques and automates the design of outsourced algorithms for several encryption schemes in the literature. The outsourced schemes we have generated and analyzed with CloudSource may prove useful for limited embedded medical devices.
  • Autogroup is a new, general purpose compiler for automatically optimizing encryption and signature schemes for specific application requirements. This tool is complementary to CloudSource but focuses on how pairing-based cryptographic schemes can be instantiated in certain groups which are more efficient for implementation.

• Focus of the research/Market need for this project
  This work will reduce the number of flaws in software used to security electronic health records. By automating the techniques, the resulting code will be much less prone to developer error. This in turn should feed the market for more secure software.

• Project Aims/Goals
  The end goal of the project is more security in healthcare IT systems, and better protection of EMRs via better encryption tools.

• Key Conclusions/Significant Findings/Milestones reached/Deliverables
  The results are being used by several researchers. Furthermore, the students who worked on this have graduated with their Ph.Ds. and moved on to industry, and they are using these techniques in their jobs and building on them.

• Materials Available for Other Investigators/interested parties
  We distributed our software to other researchers who were interested in these automated techniques. The details of our protocols and algorithms were also published in two CCS conferences.

• Market entry strategies
  By making the software available for free to the market, it is our hope that interested parties will adopt these automation techniques when building encryption mechanisms for EHRs and signature mechanisms for data streams such as those from HL7 sources.

Bibliography
Automatically Generating Outsourced Decryption for Pairing-based Encryption Schemes
Joseph Ayo Akinyele, Matthew W. Pagano, Matthew Green and Avi Rubin
Under Review, 2014

Using SMT Solvers to Automate Design Tasks for Encryption and Signature Schemes
Joseph Ayo Akinyele, Matthew D. Green, and Susan Hohenberger
Proceedings of the 20th ACM CCS, November 2013