Neha Rungta is a senior principal applied scientist in the Automated Reasoning Group with Amazon Web Services (AWS), working on formal verification techniques for cloud security. Prior to joining AWS, Rungta was already well-known for her work on symbolic execution, automated program analysis, and airspace modeling at the NASA Ames Research Center. She earned a PhD in computer science from Brigham Young University in 2009.
Amazon Science recently spoke with Rungta about her career path and her work on automated reasoning.
Q. Tell us about your career path.
When I was an undergraduate at BYU, I started to think, ‘OK, what should I be doing?’ Some people have their entire careers laid out, along with what they want in life. I’m not that kind of person. I’m really more of an ‘explorer.’ I’m attracted to the unknown — my parents encouraged me to follow my own path.
So, I joined the research lab that was related to doing automated reasoning as an undergrad. I didn’t know anything about automated reasoning, but that was part of the attraction for me — that I didn’t know what it was and wanted to learn more about it.
At the time, people in my research lab were collaborating with some folks at NASA Ames. They said to me, ‘It would be great for you to present the work you’re doing on directed model checking to scientists at Ames.’ I flew to California and did a presentation. That’s when I first got know more about the work they were doing and it was inspiring — it was much more than rockets and airplanes. It was about how to prove they were correct. And that was when I started thinking I should pursue a graduate degree in automated reasoning.”
Q. Automated reasoning is used widely within AWS to improve cloud security. How does it work?
How Amazon’s automated reasoning team uses formal verification methods
Automated reasoning is a way to get comprehensive visibility into the security of a system. It uses rules about a system to logically infer its future behaviors. It doesn’t try to look at historical data to predict an answer. Instead it analyzes models of systems to prove its correctness. The models are of systems, code, and configurations. For example, it analyzes access control policies to determine who has access to a system, and who does not.
It empowers customers to make decisions about what access is intentional versus not. You don’t have to be a security expert, or even know how access control works, or be like a mathematician or a logician.
Q. What attracted you to Amazon?
NASA was at the time a dream job for me. I had a great time, and it really was good for my exploration instinct. After a few years, I decided I could keep doing what I was doing or take on a new challenge. The biggest attraction for me at Amazon was the chance to build something from the ground up. Even though Amazon is a big company, at times it can feel as if you’re the third or fourth person to join a startup.
I like the fact we take on real-world challenges that are relevant to millions of customers. And the scale is impressive — almost unimaginable. We work with things that impact millions and millions of customers. For example, when we launched Access Analyzer (a tool that helps customers control access and permissions to their AWS services and resources), we had a very positive response from customers because it allowed them to detect unintended access with a click of a few buttons. And they could leverage it without having to know what’s going on under the hood.
Being at Amazon gives us a tight feedback loop. You have customers telling you, ’Oh, this is great — it’s helping us make our network more secure.’ That’s a very powerful motivation for a scientist. I really enjoy being part of the conversation with customers and getting feedback from them and hearing about how our work is directly impacting them.
Q. What has contributed to your success at Amazon?
I don’t see the destination as the most important thing in a career journey — it’s the journey itself. And that includes making mistakes. That’s when I am able to grow and learn things.
Q. Any advice for someone who would like to make an impact at a company such as Amazon?
I would tell them to really dive in and learn about the pain points of Amazon’s customers. Focus on the problem. Once they do, they won’t have to ask themselves, ‘What’s my next idea?’ because it will be right in front of them.
Take ownership of your work and push for the right things. Amazon is a place where you’re essentially master of your own destiny. If you’re driven and motivated, the world is your oyster.
Q. What’s the “must read” research paper or book a student interested in automated reasoning should read?
“Decision Procedures: An Algorithmic Point of View,” by Daniel Kroening and Ofer Strichman.
It’s a great introduction to decision procedures — problems that end with a correct answer of yes or no. These sorts of problems are commonly used in automated reasoning and fields such as theorem-proving and compiler optimization.
