Demystify Your Trust Boundary With Interactive Refinement
| Automated reasoning can precisely answer questions about system behavior, but traditionally requires a huge up-front investment. The traditional approach begins with asking the user to provide a complete formal specification, which can be expensive in time and effort. It then checks if the implementation matches the specification, providing value to its user at the end of this process. In our case, we are particularly interested in the specification of architectural trust boundaries for data. Here, the traditional approach calls for users to provide their complete formal trust boundary upfront. We flip this around. We present a way for users to explore and build their trust boundary incrementally, thus delivering value to the user with every increment. We use this approach to help security engineers better understand the attack surface of consumer payments applications at Amazon. |
Consumer payments applications process and store sensitive data, such as credit card numbers, that should never leave the trust boundary. Our tool provides a foundation for security engineers and application developers to maintain the trust boundary of these applications without requiring any knowledge of automated reasoning. We present a tool that implements this approach and explain the automated reasoning that powers it.
Vaibhav Sharma is an Applied Scientist at Amazon.com Services LLC. Vaibhav works on applying automated reasoning to secure payments applications at Amazon. Previously, Vaibhav worked on applying automated reasoning to the Internet of Things (IoT) domain at AWS. Prior to AWS, Vaibhav obtained a PhD in Computer Science from the University of Minnesota during which he worked on program synthesis using scalable symbolic execution.