How we built Cedar with automated reasoning and differential testing

The new development process behind Amazon Web Services’ Cedar authorization-policy language.

Cedar is a new authorization-policy language used by the Amazon Verified Permissions and AWS Verified Access managed services, and we recently released it publicly. Using Cedar, developers can write policies that specify fine-grained permissions for their applications. The applications then authorize access requests by calling Cedar’s authorization engine. Because Cedar policies are separate from application code, they can be independently authored, updated, analyzed, and audited. 

Related content
CAV keynote lecture by the director of applied science for AWS Identity explains how AWS is making the power of automated reasoning available to all customers.

We want to assure developers that Cedar’s authorization decisions will be correct. To provide that assurance, we follow a two-part process we call verification-guided development when we’re working on Cedar. First, we use automated reasoning to prove important correctness properties about formal models of Cedar’s components. Second, we use differential random testing to show that the models match the production code. In this blog post we present an overview of verification-guided development for Cedar.

A primer on Cedar

Cedar is a language for writing and enforcing authorization policies for custom applications. Cedar policies are expressed in syntax resembling natural language. They define who (the principal) can do what (the action) on what target (the resource) under which conditions (when)?

To see how Cedar works, consider a simple application, TinyTodo, designed for managing task lists. TinyTodo uses Cedar to control who can do what. Here is one of TinyTodo’s policies:

// policy 1
permit(principal, action, resource)
when {
	resource has owner && resource.owner == principal
};

This policy states that any principal (a TinyTodo User) can perform any action on any resource (a TinyTodo List) as long as the resource’s creator, defined by its owner attribute, matches the requesting principal. Here’s another TinyTodo Cedar policy:

// policy 2
permit (
	principal,
	action == Action::"GetList",
	resource
)
when {
	principal in resource.editors || principal in resource.readers
};

This policy states that any principal can read the contents of a task list (Action::"GetList") if that principal is in either the list’s readers group or its editors group. Here is a third policy:

// policy 3
forbid (
	principal in Team::"interns",
	action == Action::"CreateList",
	resource == Application::"TinyTodo"
);

This policy states that any principal who is an intern (in Team::"interns") is forbidden from creating a new task list (Action::"CreateList") using TinyTodo (Application::"TinyTodo").

Related content
Meet Amazon Science’s newest research area.

When the application needs to enforce access, as when a user of TinyTodo issues a command, it only needs to make a corresponding request to the Cedar authorization engine. The authorization engine evaluates the request in light of the Cedar policies and relevant application data. If it returns decision Allow, TinyTodo can proceed with the command. If it returns decision Deny, TinyTodo can report that the command is not permitted.

How do we build Cedar to be trustworthy?

Our work on Cedar uses a process we call verification-guided development to ensure that Cedar’s authorization engine makes the correct decisions. The process has two parts. First, we model Cedar’s authorization engine and validator in the Dafny verification-aware programming language. With Dafny, you can write code, and you can specify properties about what the code is meant to do under all circumstances. Using Dafny’s built-in automated-reasoning capabilities we have proved that the code satisfies a variety of safety and security properties.

Second, we use differential random testing (DRT) to confirm that Cedar’s production implementation, written in Rust, matches the Dafny model’s behavior. We generate millions of diverse inputs and feed them to both the Dafny model and the production code. If both versions always produce the same output, we have a high degree of confidence that the implementation matches the model.

Cedar figure.png
Building Cedar using automated reasoning and differential testing.

Proving properties about Cedar authorization

 Cedar’s authorization algorithm was designed to be secure by default, as exemplified by the following two properties:

  • explicit permit — permission is granted only by individual permit policies and is not gained by error or default;
  • forbid overrides permit — any applicable forbid policy always denies access, even if there is a permit policy that allows it.

With these properties, sets of policies are easier to understand. Policy authors know that permit policies are the only way access is granted, and forbid policies decline access regardless of whether it is explicitly permitted.

Related content
Distributing proof search, reasoning about distributed systems, and automating regulatory compliance are just three fruitful research areas.

Given an authorization request, the Cedar authorization engine takes each Cedar policy and evaluates it after substituting the application request parameters into the principal, action and resource variables. For example, for the request principal= User::”Alice”, action=Action::”GetList”, and resource=List::”AliceList”, substituting for the variables in policy 1 would produce the expression List::”AliceList” has owner && List::”AliceList”.owner == User::”Alice”. If this expression evaluates to true, we say the request satisfies the policy. The authorization engine collects the satisfied forbid and permit policies into distinct sets and then makes its decision.

We model the authorization engine as a Dafny function and use Dafny’s automated-reasoning capabilities to state and prove the explicit-permit and forbid-overrides-permit properties. To see how this helps uncover mistakes, let’s consider a buggy version of the authorization engine:

function method isAuthorized(): Response { // BUGGY VERSION
	var f := forbids();
	var p := permits();
	if f != {} then
		Response(Deny, f)
	else
		Response(Allow, p)
}

The logic states that if any forbid policy is applicable (set f is not the empty set {}), the result should be Deny, thus overriding any applicable permit policies (in set p). Otherwise, the result is Allow. While this logic correctly reflects the desired forbid-overrides-permit property, it does not correctly capture explicit permit. Just because there are no applicable forbid policies doesn’t mean there are any applicable permit policies. We can see this by specifying and attempting to prove explicit permit in Dafny:

// A request is explicitly permitted when a permit policy is satisfied
predicate IsExplicitlyPermitted(request: Request, store: Store) {
	exists p ::
		p in store.policies.policies.Keys &&
		store.policies.policies[p].effect == Permit &&
		Authorizer(request, store).satisfied(p)
}
lemma AllowedIfExplicitlyPermitted(request: Request, store: Store)
ensures // A request is allowed if it is explicitly permitted
	(Authorizer(request, store).isAuthorized().decision == Allow) ==>
	IsExplicitlyPermitted(request, store)
{ ... }

A Dafny predicate is a function that takes arguments and returns a logical condition, and a Dafny lemma is a property to be proved. The IsExplicitlyPermitted predicate defines the condition that there is an applicable permit policy for the given request. The AllowedIfExplicitlyPermitted lemma states that a decision of Allow necessarily means the request was explicitly permitted. This lemma does not hold for the isAuthorized definition above; Dafny complains that A postcondition might not hold on this return path and points to the ensures clause.

Here is the corrected code:

function method isAuthorized(): Response {
	var f := forbids();
	var p := permits();
	if f == {} && p != {} then
		Response(Allow, p)
	else
		Response(Deny, f)
}

Now a response is Allow only if there are no applicable forbid policies, and there is at least one applicable permit policy. With this change, Dafny automatically proves AllowedIfExplicitlyPermitted. It also proves forbid overrides permit (not shown).

Related content
To mark the occasion of the eighth Federated Logic Conference (FloC), Amazon’s Byron Cook, Daniel Kröning, and Marijn Heule discussed automated reasoning’s prospects.

We have used the Cedar Dafny models to prove a variety of properties. Our most significant proof is that the Cedar validator, which confirms that Cedar policies are consistent with the application’s data model, is sound: if the validator accepts a policy, evaluating the policy should never result in certain classes of error. When carrying out this proof in Dafny, we found a number of subtle bugs in the validator’s design that we were able to correct.

We note that Dafny models are useful not just for automated reasoning but for manual reasoning, too. The Dafny code is much easier to read than the Rust implementation. As one measure of this, at the time of this writing the Dafny model for the authorizer has about one-sixth as many lines of code as the production code. Both Cedar users and tool implementers can refer to the Dafny models to quickly understand precise details about how Cedar works.

Differential random testing

Once we have proved properties about the Cedar Dafny model, we want to provide evidence that they hold for the production code, too, which we can do by using DRT to show that the model and the production code behave the same. Using the cargo fuzz random-testing framework, we generate millions of inputs — access requests, accompanying data, and policies — and send them to both the Dafny model engine and the Rust production engine. If the two versions agree on the decision, then all is well. If they disagree, then we have found a bug.

The main challenge with using DRT effectively is to ensure the necessary code coverage by generating useful and diverse inputs. Randomly generated policies are unlikely to mention the same groups and attributes chosen in randomly generated requests and data. As a result, pure random generation will miss a lot of core evaluation logic and overindex on error-handling code. To resolve this, we wrote several input generators, including ones that take care to generate policies, data, and requests that are consistent with one another, while also producing policies that use Cedar’s key language constructs. As of this writing, we run DRT for six hours nightly and execute on the order of 100 million total tests.

Related content
Rungta had a promising career with NASA, but decided the stars aligned for her at Amazon.

The use of DRT during Cedar’s development has discovered corner cases where there were discrepancies between the model and the production code, making it an important tool in our toolkit. For example, there was a bug in a Rust package we were using for IP address operations; the Dafny model exposed an issue in how the package was parsing IP addresses. Since the bug is in an external package, we fixed the problem within our code while we wait for the upstream fix. We also found subtle bugs in the Cedar policy parser, in how the authorizer handles missing application data, and how namespace prefixes on application data (e.g., TinyTodo::List::”AliceList”) are interpreted.

Learn more

In this post we have discussed the verification-guided development process we have followed for the Cedar authorization policy language. In this process, we model Cedar language components in the Dafny programming language and use Dafny’s automated-reasoning capabilities to prove properties about them. We check that the Cedar production code matches the Dafny model through differential random testing. This process has revealed several interesting bugs during development and has given us greater confidence that Cedar’s authorization engine makes correct decisions.

To learn more, you can check out the Cedar Dafny models and differential-testing code on GitHub. You can also learn more about Dafny on the Dafny website and the Cedar service on the Cedar website.

Related content

US, CA, Santa Clara
About Amazon Health Amazon Health’s mission is to make it dramatically easier for customers to access the healthcare products and services they need to get and stay healthy. Towards this mission, we (Health Storefront and Shared Tech) are building the technology, products and services, that help customers find, buy, and engage with the healthcare solutions they need. Job summary We are seeking an exceptional Applied Scientist to join a team of experts in the field of machine learning, and work together to break new ground in the world of healthcare to make personalized and empathetic care accessible, convenient, and cost-effective. We leverage and train state-of-the-art large-language-models (LLMs) and develop entirely new experiences to help customers find the right products and services to address their health needs. We work on machine learning problems for intent detection, dialogue systems, and information retrieval. You will work in a highly collaborative environment where you can pursue both near-term productization opportunities to make immediate, meaningful customer impacts while pursuing ambitious, long-term research. You will work on hard science problems that have not been solved before, conduct rapid prototyping to validate your hypothesis, and deploy your algorithmic ideas at scale. You will get the opportunity to pursue work that makes people's lives better and pushes the envelop of science. Key job responsibilities - Translate product and CX requirements into science metrics and rigorous testing methodologies. - Invent and develop scalable methodologies to evaluate LLM outputs against metrics and guardrails. - Design and implement the best-in-class semantic retrieval system by creating high-quality knowledge base and optimizing embedding models and similarity measures. - Conduct tuning, training, and optimization of LLMs to achieve a compelling CX while reducing operational cost to be scalable. A day in the life In a fast-paced innovation environment, you work closely with product, UX, and business teams to understand customer's challenges. You translate product and business requirements into science problems. You dive deep into challenging science problems, enabling entirely new ML and LLM-driven customer experiences. You identify hypothesis and conduct rapid prototyping to learn quickly. You develop and deploy models at scale to pursue productizations. You mentor junior science team members and help influence our org in scientific best practices. About the team We are the ML Science and Engineering team, with a strong focus on Generative AI. The team consists of top-notch ML Scientists with diverse background in healthcare, robotics, customer analytics, and communication. We are committed to building and deploying the most advanced scientific capabilities and solutions for the products and services at Amazon Health. We are open to hiring candidates to work out of one of the following locations: Santa Clara, CA, USA
US, WA, Seattle
We are designing the future. If you are in quest of an iterative fast-paced environment, where you can drive innovation through scientific inquiry, and provide tangible benefit to hundreds of thousands of our associates worldwide, this is your opportunity. Come work on the Amazon Worldwide Fulfillment Design & Engineering Team! We are looking for an experienced and senior Research Scientist with background in Ergonomics and Industrial Human Factors, someone that is excited to work on complex real-world challenges for which a comprehensive scientific approach is necessary to drive solutions. Your investigations will define human factor / ergonomic thresholds resulting in design and implementation of safe and efficient workspaces and processes for our associates. Your role will entail assessment and design of manual material handling tasks throughout the entire Amazon network. You will identify fundamental questions pertaining to the human capabilities and tolerances in a myriad of work environments, and will initiate and lead studies that will drive decision making on an extreme scale. .You will provide definitive human factors/ ergonomics input and participate in design with every single design group in our network, including Amazon Robotics, Engineering R&D, and Operations Engineering. You will work closely with our Worldwide Health and Safety organization to gain feedback on designs and work tenaciously to continuously improve our associate’s experience. Key job responsibilities - Collaborating and designing work processes and workspaces that adhere to human factors / ergonomics standards worldwide. - Producing comprehensive and assessments of workstations and processes covering biomechanical, physiological, and psychophysical demands. - Effectively communicate your design rationale to multiple engineering and operations entities. - Identifying gaps in current human factors standards and guidelines, and lead comprehensive studies to redefine “industry best practices” based on solid scientific foundations. - Continuously strive to gain in-depth knowledge of your profession, as well as branch out to learn about intersecting fields, such as robotics and mechatronics. - Travelling to our various sites to perform thorough assessments and gain in-depth operational feedback, approximately 25%-50% of the time. We are open to hiring candidates to work out of one of the following locations: Seattle, WA, USA
GB, London
Amazon Advertising is looking for a Data Scientist to join its brand new initiative that powers Amazon’s contextual advertising products. Advertising at Amazon is a fast-growing multi-billion dollar business that spans across desktop, mobile and connected devices; encompasses ads on Amazon and a vast network of hundreds of thousands of third party publishers; and extends across US, EU and an increasing number of international geographies. The Supply Quality organization has the charter to solve optimization problems for ad-programs in Amazon and ensure high-quality ad-impressions. We develop advanced algorithms and infrastructure systems to optimize performance for our advertisers and publishers. We are focused on solving a wide variety of problems in computational advertising like traffic quality prediction (robot and fraud detection), Security forensics and research, Viewability prediction, Brand Safety, Contextual data processing and classification. Our team includes experts in the areas of distributed computing, machine learning, statistics, optimization, text mining, information theory and big data systems. We are looking for a dynamic, innovative and accomplished Data Scientist to work on data science initiatives for contextual data processing and classification that power our contextual advertising solutions. Are you an experienced user of sophisticated analytical techniques that can be applied to answer business questions and chart a sustainable vision? Are you exited by the prospect of communicating insights and recommendations to audiences of varying levels of technical sophistication? Above all, are you an innovator at heart and have a track record of resolving ambiguity to deliver result? As a data scientist, you help our data science team build cutting edge models and measurement solutions to power our contextual classification technology. As this is a new initiative, you will get an opportunity to act as a thought leader, work backwards from the customer needs, dive deep into data to understand the issues, define metrics, conceptualize and build algorithms and collaborate with multiple cross-functional teams. Key job responsibilities * Define a long-term science vision for contextual-classification tech, driven fundamentally from the needs of our advertisers and publishers, translating that direction into specific plans for the science team. Interpret complex and interrelated data points and anecdotes to build and communicate this vision. * Collaborate with software engineering teams to Identify and implement elegant statistical and machine learning solutions * Oversee the design, development, and implementation of production level code that handles billions of ad requests. Own the full development cycle: idea, design, prototype, impact assessment, A/B testing (including interpretation of results) and production deployment. * Promote the culture of experimentation and applied science at Amazon. * Demonstrated ability to meet deadlines while managing multiple projects. * Excellent communication and presentation skills working with multiple peer groups and different levels of management * Influence and continuously improve a sustainable team culture that exemplifies Amazon’s leadership principles. We are open to hiring candidates to work out of one of the following locations: London, GBR
JP, 13, Tokyo
We are seeking a Principal Economist to be the science leader in Amazon's customer growth and engagement. The wide remit covers Prime, delivery experiences, loyalty program (Amazon Points), and marketing. We look forward to partnering with you to advance our innovation on customers’ behalf. Amazon has a trailblazing track record of working with Ph.D. economists in the tech industry and offers a unique environment for economists to thrive. As an economist at Amazon, you will apply the frontier of econometric and economic methods to Amazon’s terabytes of data and intriguing customer problems. Your expertise in building reduced-form or structural causal inference models is exemplary in Amazon. Your strategic thinking in designing mechanisms and products influences how Amazon evolves. In this role, you will build ground-breaking, state-of-the-art econometric models to guide multi-billion-dollar investment decisions around the global Amazon marketplaces. You will own, execute, and expand a research roadmap that connects science, business, and engineering and contributes to Amazon's long term success. As one of the first economists outside North America/EU, you will make an outsized impact to our international marketplaces and pioneer in expanding Amazon’s economist community in Asia. The ideal candidate will be an experienced economist in empirical industrial organization, labour economics, or related structural/reduced-form causal inference fields. You are a self-starter who enjoys ambiguity in a fast-paced and ever-changing environment. You think big on the next game-changing opportunity but also dive deep into every detail that matters. You insist on the highest standards and are consistent in delivering results. Key job responsibilities - Work with Product, Finance, Data Science, and Data Engineering teams across the globe to deliver data-driven insights and products for regional and world-wide launches. - Innovate on how Amazon can leverage data analytics to better serve our customers through selection and pricing. - Contribute to building a strong data science community in Amazon Asia. We are open to hiring candidates to work out of one of the following locations: Tokyo, 13, JPN
DE, BE, Berlin
Ops Integration: Concessions team is looking for a motivated, creative and customer obsessed Snr. Applied Scientist with a strong machine learning background, to develop advanced analytics models (Computer Vision, LLMs, etc.) that improve customer experiences We are the voice of the customer in Amazon’s operations, and we take that role very seriously. If you join this team, you will be a key contributor to delivering the Factory of the Future: leveraging Internet of Things (IoT) and advanced analytics to drive tangible, operational change on the ground. You will collaborate with a wide range of stakeholders (You will partner with Research and Applied Scientists, SDEs, Technical Program Managers, Product Managers and Business Leaders) across the business to develop and refine new ways of assessing challenges within Amazon operations. This role will combine Amazon’s oldest Leadership Principle, with the latest analytical innovations, to deliver business change at scale and efficiently The ideal candidate will have deep and broad experience with theoretical approaches and practical implementations of vision techniques for task automation. They will be a motivated self-starter who can thrive in a fast-paced environment. They will be passionate about staying current with sensing technologies and algorithms in the broader machine vision industry. They will enjoy working in a multi-disciplinary team of engineers, scientists and business leaders. They will seek to understand processes behind data so their recommendations are grounded. Key job responsibilities Your solutions will drive new system capabilities with global impact. You will design highly scalable, large enterprise software solutions involving computer vision. You will develop complex perception algorithms integrating across multiple sensing devices. You will develop metrics to quantify the benefits of a solution and influence project resources. You will validate system performance and use insights from your live models to drive the next generation of model development. Common tasks include: • Research, design, implement and evaluate complex perception and decision making algorithms integrating across multiple disciplines • Work closely with software engineering teams to drive scalable, real-time implementations • Collaborate closely with team members on developing systems from prototyping to production level • Collaborate with teams spread all over the world • Track general business activity and provide clear, compelling management reports on a regular basis We are open to hiring candidates to work out of one of the following locations: Berlin, BE, DEU | Berlin, DEU
DE, BY, Munich
Ops Integration: Concessions team is looking for a motivated, creative and customer obsessed Snr. Applied Scientist with a strong machine learning background, to develop advanced analytics models (Computer Vision, LLMs, etc.) that improve customer experiences We are the voice of the customer in Amazon’s operations, and we take that role very seriously. If you join this team, you will be a key contributor to delivering the Factory of the Future: leveraging Internet of Things (IoT) and advanced analytics to drive tangible, operational change on the ground. You will collaborate with a wide range of stakeholders (You will partner with Research and Applied Scientists, SDEs, Technical Program Managers, Product Managers and Business Leaders) across the business to develop and refine new ways of assessing challenges within Amazon operations. This role will combine Amazon’s oldest Leadership Principle, with the latest analytical innovations, to deliver business change at scale and efficiently The ideal candidate will have deep and broad experience with theoretical approaches and practical implementations of vision techniques for task automation. They will be a motivated self-starter who can thrive in a fast-paced environment. They will be passionate about staying current with sensing technologies and algorithms in the broader machine vision industry. They will enjoy working in a multi-disciplinary team of engineers, scientists and business leaders. They will seek to understand processes behind data so their recommendations are grounded. Key job responsibilities Your solutions will drive new system capabilities with global impact. You will design highly scalable, large enterprise software solutions involving computer vision. You will develop complex perception algorithms integrating across multiple sensing devices. You will develop metrics to quantify the benefits of a solution and influence project resources. You will validate system performance and use insights from your live models to drive the next generation of model development. Common tasks include: • Research, design, implement and evaluate complex perception and decision making algorithms integrating across multiple disciplines • Work closely with software engineering teams to drive scalable, real-time implementations • Collaborate closely with team members on developing systems from prototyping to production level • Collaborate with teams spread all over the world • Track general business activity and provide clear, compelling management reports on a regular basis We are open to hiring candidates to work out of one of the following locations: Munich, BE, DEU | Munich, BY, DEU | Munich, DEU
IT, MI, Milan
Ops Integration: Concessions team is looking for a motivated, creative and customer obsessed Snr. Applied Scientist with a strong machine learning background, to develop advanced analytics models (Computer Vision, LLMs, etc.) that improve customer experiences We are the voice of the customer in Amazon’s operations, and we take that role very seriously. If you join this team, you will be a key contributor to delivering the Factory of the Future: leveraging Internet of Things (IoT) and advanced analytics to drive tangible, operational change on the ground. You will collaborate with a wide range of stakeholders (You will partner with Research and Applied Scientists, SDEs, Technical Program Managers, Product Managers and Business Leaders) across the business to develop and refine new ways of assessing challenges within Amazon operations. This role will combine Amazon’s oldest Leadership Principle, with the latest analytical innovations, to deliver business change at scale and efficiently The ideal candidate will have deep and broad experience with theoretical approaches and practical implementations of vision techniques for task automation. They will be a motivated self-starter who can thrive in a fast-paced environment. They will be passionate about staying current with sensing technologies and algorithms in the broader machine vision industry. They will enjoy working in a multi-disciplinary team of engineers, scientists and business leaders. They will seek to understand processes behind data so their recommendations are grounded. Key job responsibilities Your solutions will drive new system capabilities with global impact. You will design highly scalable, large enterprise software solutions involving computer vision. You will develop complex perception algorithms integrating across multiple sensing devices. You will develop metrics to quantify the benefits of a solution and influence project resources. You will validate system performance and use insights from your live models to drive the next generation of model development. Common tasks include: • Research, design, implement and evaluate complex perception and decision making algorithms integrating across multiple disciplines • Work closely with software engineering teams to drive scalable, real-time implementations • Collaborate closely with team members on developing systems from prototyping to production level • Collaborate with teams spread all over the world • Track general business activity and provide clear, compelling management reports on a regular basis We are open to hiring candidates to work out of one of the following locations: Milan, MI, ITA
ES, M, Madrid
Ops Integration: Concessions team is looking for a motivated, creative and customer obsessed Snr. Applied Scientist with a strong machine learning background, to develop advanced analytics models (Computer Vision, LLMs, etc.) that improve customer experiences We are the voice of the customer in Amazon’s operations, and we take that role very seriously. If you join this team, you will be a key contributor to delivering the Factory of the Future: leveraging Internet of Things (IoT) and advanced analytics to drive tangible, operational change on the ground. You will collaborate with a wide range of stakeholders (You will partner with Research and Applied Scientists, SDEs, Technical Program Managers, Product Managers and Business Leaders) across the business to develop and refine new ways of assessing challenges within Amazon operations. This role will combine Amazon’s oldest Leadership Principle, with the latest analytical innovations, to deliver business change at scale and efficiently The ideal candidate will have deep and broad experience with theoretical approaches and practical implementations of vision techniques for task automation. They will be a motivated self-starter who can thrive in a fast-paced environment. They will be passionate about staying current with sensing technologies and algorithms in the broader machine vision industry. They will enjoy working in a multi-disciplinary team of engineers, scientists and business leaders. They will seek to understand processes behind data so their recommendations are grounded. Key job responsibilities Your solutions will drive new system capabilities with global impact. You will design highly scalable, large enterprise software solutions involving computer vision. You will develop complex perception algorithms integrating across multiple sensing devices. You will develop metrics to quantify the benefits of a solution and influence project resources. You will validate system performance and use insights from your live models to drive the next generation of model development. Common tasks include: • Research, design, implement and evaluate complex perception and decision making algorithms integrating across multiple disciplines • Work closely with software engineering teams to drive scalable, real-time implementations • Collaborate closely with team members on developing systems from prototyping to production level • Collaborate with teams spread all over the world • Track general business activity and provide clear, compelling management reports on a regular basis We are open to hiring candidates to work out of one of the following locations: Madrid, ESP | Madrid, M, ESP
US, CA, San Diego
The Private Brands team is looking for an Applied Scientist to join the team in building science solutions at scale. Our team applies Optimization, Machine Learning, Statistics, Causal Inference, and Econometrics/Economics to derive actionable insights. We are an interdisciplinary team of Scientists, Engineers, and Economists and primary focus on building optimization and machine learning solutions in supply chain domain with specific focus on Amazon private brand products. Key job responsibilities You will work with business leaders, scientists, and economists to translate business and functional requirements into concrete deliverables, including the design, development, testing, and deployment of highly scalable optimization solutions and ML models. This is a unique, high visibility opportunity for someone who wants to have business impact, dive deep into large-scale problems, enable measurable actions on the consumer economy, and work closely with scientists and economists. As a scientist, you bring business and industry context to science and technology decisions. You set the standard for scientific excellence and make decisions that affect the way we build and integrate algorithms. Your solutions are exemplary in terms of algorithm design, clarity, model structure, efficiency, and extensibility. You tackle intrinsically hard problems, acquiring expertise as needed. You decompose complex problems into straightforward solutions. We are particularly interested in candidates with experience in predictive and machine learning models and working with distributed systems. Academic and/or practical background in Machine Learning are particularly relevant for this position. Familiarity and experience in applying Operations Research techniques to supply chain problems is a plus. To know more about Amazon science, Please visit https://www.amazon.science We are open to hiring candidates to work out of one of the following locations: San Diego, CA, USA | Seattle, WA, USA
LU, Luxembourg
Ops Integration: Concessions team is looking for a motivated, creative and customer obsessed Snr. Applied Scientist with a strong machine learning background, to develop advanced analytics models (Computer Vision, LLMs, etc.) that improve customer experiences We are the voice of the customer in Amazon’s operations, and we take that role very seriously. If you join this team, you will be a key contributor to delivering the Factory of the Future: leveraging Internet of Things (IoT) and advanced analytics to drive tangible, operational change on the ground. You will collaborate with a wide range of stakeholders (You will partner with Research and Applied Scientists, SDEs, Technical Program Managers, Product Managers and Business Leaders) across the business to develop and refine new ways of assessing challenges within Amazon operations. This role will combine Amazon’s oldest Leadership Principle, with the latest analytical innovations, to deliver business change at scale and efficiently The ideal candidate will have deep and broad experience with theoretical approaches and practical implementations of vision techniques for task automation. They will be a motivated self-starter who can thrive in a fast-paced environment. They will be passionate about staying current with sensing technologies and algorithms in the broader machine vision industry. They will enjoy working in a multi-disciplinary team of engineers, scientists and business leaders. They will seek to understand processes behind data so their recommendations are grounded. Key job responsibilities Your solutions will drive new system capabilities with global impact. You will design highly scalable, large enterprise software solutions involving computer vision. You will develop complex perception algorithms integrating across multiple sensing devices. You will develop metrics to quantify the benefits of a solution and influence project resources. You will validate system performance and use insights from your live models to drive the next generation of model development. Common tasks include: • Research, design, implement and evaluate complex perception and decision making algorithms integrating across multiple disciplines • Work closely with software engineering teams to drive scalable, real-time implementations • Collaborate closely with team members on developing systems from prototyping to production level • Collaborate with teams spread all over the world • Track general business activity and provide clear, compelling management reports on a regular basis We are open to hiring candidates to work out of one of the following locations: Luxembourg, LUX