Automated Reasoning
AWS has invested in automated reasoning as a way to provide higher security assurance at scale.
Hendra Su/Getty Images/iStockphoto

How AWS’s Automated Reasoning Group helps make AWS and other Amazon products more secure

Amazon scientists are on the cutting edge of using math-based logic to provide better network security, access management, and greater reliability.

Data breaches have seemingly become part of everyday digital life. In the past few years many large financial services firms, among others, have been hit with data breaches. In fact, the research firm Risk Based Security reports that in the first nine months of 2019, medical services, retailers, and government agencies suffered 5,183 data breaches, opening 7.9 billion records to theft or other nefarious purposes.

Security is the top priority for AWS, the world’s most comprehensive and broadly adopted cloud platform. In addition to an abundance of security resources and expert guidance, AWS has a (not so) secret weapon that helps protect the company and its customers—automated reasoning. Automated reasoning applications help detect against unauthorized access, improve network security, and ensure software compatibility.

Byron Cook
Byron Cook, ARG senior principal scientist

In response to the rapid scale of cloud growth, AWS invested in automated reasoning as a way to provide higher security assurance at scale. Five years ago, Byron Cook, senior principal scientist, established the Automated Reasoning Group (ARG) within AWS. Considered by many as the strongest team in its field, ARG began to create and implement automated reasoning tools to secure AWS’s own infrastructure and services, as well as those of AWS customers.

Automated reasoning is a sub-field of artificial intelligence; it applies mathematical analysis to better understand complex computer systems or large code bases. The technique takes a system and a question you might have about the system—like “is the system memory safe?”—and reformulates the question as a set of mathematical properties.

While AI is very good at sorting unstructured data – picking out photos of cats from thousands of animal photos, for instance – automated reasoning can be used for more abstract and less clearly defined tasks, such as who should or should not have access to a certain set of data.

Data security is certainly one of the top three pain points for the tech industry...It has been a priority of ours to put features in place to make sure our AWS customers’ resource policies are correctly configured.
Byron Cook, ARG senior principal scientist

In software development, automated reasoning replaces laborious and possible flawed testing with a rigorous mathematical proof that the software will function properly and securely, such as ensuring that data structures are correct.

“Automated reasoning is a way to quickly analyze infinite or very large-scale state spaces,” says Cook. “It does so by using high-school algebra to push symbols around.”

In concept, automated reasoning dates to the 19th century and the work of George Boole, whose work on Boolean Logic – with its variables of true and false – laid the foundation for all modern programming languages.

“Automated reasoning doesn’t look at data, but instead looks for things where we know there is a definite set of rules,” adds Neha Rungta, a senior principal applied scientist and former NASA research scientist. "It asks, ‘Given our specifications, is there a case where something unexpected can happen?’

Neha Rungta
Neha Rungta works on formal verification techniques for cloud security within the Amazon Web Services Automated Reasoning Group.

“It doesn’t need data, or logs, or who has accessed things in the past. It just looks at your configurations [and] your policies. Because of the rules we’ve encoded, it can very quickly tell you who outside your account has access.”

In just a few years, the team’s automated reasoning tools have been applied to a broad range of challenges in networking, access control permissions, automated compliance verification, and analyzing code bases for some of AWS’s most prominent services. Most recently, ARG released a new service capability called IAM Access Analyzer. Access Analyzer is a capability of AWS IAM, and makes it easier for customers to spot holes in their policies that would grant overly broad access to their resources or data. In turn, security teams use these findings to determine whether this introduces unintended risk.

For example, policies may prohibit engineers from accessing a company’s key financial information, or financial people from seeing engineers’ work. IAM Access Analyzer applies logic and mathematical inference to determine all possible access paths allowed by a resource policy. Once the policy is written, IAM Access Analyzer monitors data pathways without human intervention.

Automated reasoning is also under the hood of Amazon S3, providing industry-leading security to Amazon’s popular cloud-storage service.

Says Cook: “Data security is certainly one of the top three pain points for the tech industry – a headline about a data breach in a newspaper is pretty much a daily occurrence. It has been a priority of ours to put features in place to make sure our AWS customers’ resource policies are correctly configured.”

Jim Christy
Jim Christy, software development manager, Prime Video

In addition to AWS, automated reasoning is being used across Amazon. Amazon Prime Video, for instance, uses the technology to check software updates to ensure the update doesn’t “break” a user’s device – a challenging task given all the devices now available.

”Our automated code review analyzer, Coastguard, uses automated reasoning to help third-party device manufacturers integrate Prime Video’s app correctly, before their devices hit stores or customer’s homes,” says Jim Christy, software development manager for Prime Video. “Getting the native client code right the first time is mission critical. Coastguard analyzes third-party integration code and detects when it has integrated incorrectly.”

Interest in automated reasoning solutions is increasing, especially now as more businesses transition workloads to the cloud as a result of the coronavirus pandemic.

“Automated reasoning helps our customers maintain security as they scale up,” says Reto Kramer, ARG director. “Lots of our users want to focus on their own business problems, not understanding the nuances of resources policies. With automated reasoning, we can give them cloud security that they’re comfortable with. It has really been a game-changer.”

Reto Kramer
Reto Kramer, ARG director

Since its inception, ARG has invested both in conferences focused on automated reasoning (FMCAD, PLDI, etc.) and specific professors that are pushing the edges of the field. By hiring a diverse class of interns annually, ARG has influenced the makeup of the field and built strong ties across the community. In 2018, ARG launched an initiative called Provable Security, a collective reference to the tools, features, thought leadership and community of experts in the automated reasoning field that had made their way to ARG.

“We have the dream team,” Cook says. “At AWS we have perhaps 50 PhD interns this year alone, with seven different teams doing work. We’ve hired some of the foremost practitioners in the world; individuals with backgrounds at NASA, and similar organizations."

Adds Rungta: “Automated reasoning has caused a shift in the mindset of our engineers. I get emails every day from engineers asking, ‘Can we use automated reasoning for my project?’ Its power is that you don’t have to test things and hope it works. If you run an automated reasoning tool your task will always be accomplished as specified.”

She predicts automated reasoning will have a huge impact on technology in the years to come, not only in fields such as cloud security, but in machine learning, threat detection, autonomous vehicles or aircraft, the Internet of Things, and much more.

“We’re just at the start of this journey,” says Rungta. “In a hyper-connected world, automated reasoning will be so integral that we won’t even be talking about what it is, just like nobody asks today, ‘What is the internet?’ It will just be part of the system.”

Want to learn more about automated reasoning? Watch this video from AWS re:Invent 2019 where Rungta explains more about how automated reasoning works.

Related content

US, CA, Palo Alto
The Amazon Search team creates powerful, customer-focused search and advertising solutions and technologies. Whenever a customer visits an Amazon site worldwide and types in a query or browses through product categories, the Amazon Search services go to work. We design, develop, and deploy high performance, fault-tolerant distributed search systems used by millions of Amazon customers every day. Our team works to maximize the quality and effectiveness of the search experience for visitors to Amazon websites worldwide.
JP, Tokyo
The Amazon Logistics (AMZL) Team is responsible for the acquisition, design, construction, and management of all facilities in the Amazon Delivery Station Network. AMZL is looking for a talented and passionate Data Scientist to help shape its Last Mile business with technical strategies and solutions, by processing, analyzing and interpreting huge data sets. You should be comfortable with ambiguity, problem solving and enjoy working in a fast-paced, diverse and dynamic environment. Using analytical rigor and statistical methods, you mine through data to identify opportunities for Amazon and our delivery channels. And you collaborate with other scientists, engineers, Product and Program Managers to deploy new products and solutions. [More Information] Last Mile Department Data Analyst/BI Engineer Tokyo Office *Amazon is committed to a diverse and inclusive workplace. Amazon is an equal opportunity employer and does not discriminate on the basis of race, national origin, gender, gender identity, sexual orientation, protected veteran status, disability, age, or other legally protected status. For individuals with disabilities who would like to request an accommodation, visit https://www.amazon.jobs/disability/jp Key job responsibilities Creating a roadmap of the most challenging business questions and use data to articulate possible root cause analysis and solutions Managing and executing entire projects or components of large projects from start to finish including project management, data gathering and manipulation, synthesis and modeling, problem solving, and communication of insights Partnering with Product, Program and Engineering teams to design and run models, research new algorithms, and prove incrementality and drive growth Understanding drivers, impacts, and key influences on seller growth dynamics Developing and scaling end-to-end ML Models and solutions Automating feedback loops for algorithms in production Utilizing Amazon systems and tools to effectively work with terabytes of data About the team Last Mile Execution Analytics (LMEA) team of JP works as an integral part of Amazon Logistics to ensure that its business intelligence, analytics, tools and planning needs are met. By providing information, insight, and decision support, we strive to enable success of all parts of AMZL. Our customer set includes senior management, station operations, external vendors, long-term planning, Ops technology (Voice of the Delivery Station, Voice of the Customer), network planning, and pretty much every BI and Ops teams. Voice of Employee [Work Life Harmony] We believe, it is important to spend private time such as spending time with your family or doing anything you like to spur innovation. Amazon promotes a fulfilling and flexible work style according to the work volume and lifestyle of each employee.
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
LU, Luxembourg
Are you a talented and inventive scientist with a strong passion about modern data technologies and interested to improve business processes, extracting value from the data? Would you like to be a part of an organization that is aiming to use self-learning technology to process data in order to support the management of the procurement function? The Global Procurement Technology, as a part of Global Procurement Operations, is seeking a skilled Data Scientist to help build its future data intelligence in business ecosystem, working with large distributed systems of data and providing Machine Learning (ML) and Predictive Modeling expertise. You will be a member of the Data Engineering and ML Team, joining a fast-growing global organization, with a great vision to transform the Procurement field, and become the role model in the market. This team plays a strategic role supporting the core Procurement business domains as well as it is the cornerstone of any transformation and innovation initiative. Our mission is to provide a high-quality data environment to facilitate process optimization and business digitalization, on a global scale. We are supporting business initiatives, including but not limited to, strategic supplier sourcing (e.g. contracting, negotiation, spend analysis, market research, etc.), order management, supplier performance, etc. We are seeking an individual who can thrive in a fast-paced work environment, be collaborative and share knowledge and experience with his colleagues. You are expected to deliver results, but at the same time have fun with your teammates and enjoy working in the company. In Amazon, you will find all the resources required to learn new skills, grow your career, and become a better professional. You will connect with world leaders in your field and you will be tackling Data Science challenges to ensure business continuity, by taking the right decisions for your customers. As a Data Scientist in the team, you will: -be the subject matter expert to support team strategies that will take Global Procurement Operations towards world-class predictive maintenance practices and processes, driving more effective procurement functions, e.g. supplier segmentation, negotiations, shipping supplies volume forecast, spend management, etc. -have strong analytical skills and excel in the design, creation, management, and enterprise use of large data sets, combining raw data from different sources -provide technical expertise to support the development of ML models to facilitate intelligent digital services, such as Contract Lifecycle Management (CLM) and Negotiations platform -cooperate closely with different groups of stakeholders, e.g. data/software engineers, product/program managers, analysts, senior leadership, etc. to evaluate business needs and objectives to set up the best data management environment -create and share with audiences of varying levels technical papers and presentations -deal with ambiguity, prioritizing needs, and delivering results in a dynamic environment Basic qualifications -Master’s Degree in Computer Science/Engineering, Informatics, Mathematics, or a related technical discipline -3+ years of industry experience in data engineering/science, business intelligence or related field -3+ years experience in algorithm design, engineering and implementation for very-large scale applications to solve real problems -Very good knowledge of data modeling and evaluation -Very good understanding of regression modeling, forecasting techniques, time series analysis, machine-learning concepts such as supervised and unsupervised learning, classification, random forest, etc. -SQL and query performance tuning skills Preferred qualifications -2+ years of proficiency in using R, Python, Scala, Java or any modern language for data processing and statistical analysis -Experience with various RDBMS, such as PostgreSQL, MS SQL Server, MySQL, etc. -Experience architecting Big Data and ML solutions with AWS products (Redshift, DynamoDB, Lambda, S3, EMR, SageMaker, Lex, Kendra, Forecast etc.) -Experience articulating business questions and using quantitative techniques to arrive at a solution using available data -Experience with agile/scrum methodologies and its benefits of managing projects efficiently and delivering results iteratively -Excellent written and verbal communication skills including data visualization, especially in regards to quantitative topics discussed with non-technical colleagues
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
US, CA, San Francisco
About Twitch Launched in 2011, Twitch is a global community that comes together each day to create multiplayer entertainment: unique, live, unpredictable experiences created by the interactions of millions. We bring the joy of co-op to everything, from casual gaming to world-class esports to anime marathons, music, and art streams. Twitch also hosts TwitchCon, where we bring everyone together to celebrate, learn, and grow their personal interests and passions. We’re always live at Twitch. Stay up to date on all things Twitch on Linkedin, Twitter and on our Blog. About the role: Twitch builds data-driven machine learning solutions across several rich problem spaces: Natural Language Processing (NLP), Recommendations, Semantic Search, Classification/Categorization, Anomaly Detection, Forecasting, Safety, and HCI/Social Computing/Computational Social Science. As an Intern, you will work with a dedicated Mentor and Manager on a project in one of these problem areas. You will also be supported by an Advisor and participate in cohort activities such as research teach backs and leadership talks. This position can also be located in San Francisco, CA or virtual. You Will: Solve large-scale data problems. Design solutions for Twitch's problem spaces Explore ML and data research
US, WA, Seattle
We are a team of doers working passionately to apply cutting-edge advances in deep learning in the life sciences to solve real-world problems. As a Senior Applied Science Manager you will participate in developing exciting products for customers. Our team rewards curiosity while maintaining a laser-focus in bringing products to market. Competitive candidates are responsive, flexible, and able to succeed within an open, collaborative, entrepreneurial, startup-like environment. At the leading edge of both academic and applied research in this product area, you have the opportunity to work together with a diverse and talented team of scientists, engineers, and product managers and collaborate with others teams. Location is in Seattle, US Embrace Diversity Here at Amazon, we embrace our differences. We are committed to furthering our culture of inclusion. We have ten employee-led affinity groups, reaching 40,000 employees in over 190 chapters globally. We have innovative benefit offerings, and host annual and ongoing learning experiences, including our Conversations on Race and Ethnicity (CORE) and AmazeCon (gender diversity) conferences. Amazon’s culture of inclusion is reinforced within our 14 Leadership Principles, which remind team members to seek diverse perspectives, learn and be curious, and earn trust Balance Work and Life Our team puts a high value on work-life balance. It isn’t about how many hours you spend at home or at work; it’s about the flow you establish that brings energy to both parts of your life. We believe striking the right balance between your personal and professional life is critical to life-long happiness and fulfillment. We offer flexibility in working hours and encourage you to find your own balance between your work and personal lives Mentor & Grow Careers Our team is dedicated to supporting new members. We have a broad mix of experience levels and tenures, and we’re building an environment that celebrates knowledge sharing and mentorship. Our senior members enjoy one-on-one mentoring and thorough, but kind, code reviews. We care about your career growth and strive to assign projects based on what will help each team member develop into a better-rounded engineer and enable them to take on more complex tasks in the future. Key job responsibilities • Manage high performing engineering and science teams • Hire and develop top-performing engineers, scientists, and other managers • Develop and execute on project plans and delivery commitments • Work with business, data science, software engineer, biological, and product leaders to help define product requirements and with managers, scientists, and engineers to execute on them • Build and maintain world-class customer experience and operational excellence for your deliverables