Rima Tanash enrolled as a graduate student in Rice University’s Computer Science Department and registered for an elective course that sounded interesting, even though she doubted its relevance for her security research.
The CS alumna (Ph.D.’17) said, “COMP 409: Logic in Computer Science, taught by Moshe Vardi, was one of my favorite classes. The class prepares students for using logic as a formal tool in computer science, and covers topics such as: syntax, semantics, decision procedures, formal systems, and definability for both propositional and first-order logic.
“I was intrigued by propositional satisfiability solving, a.k.a. SAT, and the use of formal verification in computer science in general, but didn’t give it much thought after completing the course. Now that I am a Security Engineer for Amazon Web Services, one of my projects focuses on applying two practical security technologies that use formal verification developed by AWS.”
Tanash said data accessibility is one of the leading security concerns of cloud customers. One of the tools called Zelkova, currently in beta mode, applies semantic-based automated reasoning using satisfiability modulo theories (SMT) to reason about access policies specific to the AWS cloud.
“Using Zelkova, you can encode these access policies and formally verify they are properly configured. These policies are logical statements like, ‘Only allow users from account ‘A’ to access this storage-resource to perform a read-action.’ You can then use Zelkova to verify that no public access is allowed to this resource,” said Tanash. “Zelkova translates the policy to a first order logic formula, then uses tools including SMT solver to find requests that can satisfy the formula and check this property of the given policy.
“This is huge for our customers, because misconfigured IAM policies can lead to unintended security risks and data breaches. Zelkova provides assurance of access configurations in the cloud through the application of mathematical logic instead of the standard heuristics-based syntactic and manual checks.”
Formal verification is also used in Tiros, one of the tools Tanash deploys to answer questions about network reachability. One of the ways she can use Tiros is helping determine if a server that was intended for private use is actually reachable from the public internet. Previously this was done through penetration testing.
She said, “Unlike early pen-tests using packets, Tiros begins by capturing a snapshot of the system configuration and answers network reachability questions based on the network configuration semantics. We examine the semantics of your network configuration through formal verification rather than firing packets at it.“ Although AWS customers might still be deploying penetration tests against their infrastructure, Tiros’ use of network semantics and formal verification is new.
Tanash said, “As you can see, this breakthrough is important and comes at an exciting time. For our customers, moving their data and systems to the cloud is a big decision. They may be deploying sensitive data, and everyone wants a way to verify their network is configured securely and their access policies are correct. Amazon is using formal verification to do that.”
Formal verification is part of Amazon’s provable security initiative, and Tanash appreciates the thought processes and skills acquired in her elective class with Vardi because those same skills formed the scope of some of the work she now performs for AWS — tasks similar to those described in a video of her colleagues in the Automated Reasoning Group.
“If I hadn’t taken the logic class with Dr. Vardi, it would be hard for me to understand how these tools work, how to use them, and how to help translate access control requirements into constraint checks. It’s amazing to see how the formal method theory I learned at Rice can help solve real world problems in the cloud,” she said.
She also attributes part of her career success to skills she learned at Rice, where her research focused on social network censorship. She collected data, applied graph metrics and standard machine learning techniques, and identified censored topics and user communities. Her censorship research focused on large data sets with connected components, similar to the log-files associated with cloud storage systems.
One of the AWS projects she worked on involved utilizing access data from log-files. Breaking down her assigned project into smaller components revealed patterns she recognized from her censorship research. Tanash said, “I learned I could use graph theory–a technique I applied to my censorship research–to analyze and recommend better configurations in the cloud.
She advises current graduate students to keep an open mind about where their research skills may lead. “People don’t always hire you because you studied a specific topic, but because you have skills that you can apply to solve similar problems, and your willingness to develop new skills. It isn’t the problem you solved that’s important, but how you got the answer, what tools and mechanisms you used, and how you approached and solved the problem. That is what gets you hired.”