Stedi’s cloud EDI platform handles sensitive customer data, from business transactions like Purchase Orders and Invoices to healthcare data like Benefits Enrollments and Prior Authorizations. While we maintain a SOC 2 Type II compliance certification and our products have been certified as HIPAA-eligible by an external audit, we view these industry standards as minimum baselines and are constantly evaluating ways to elevate our security posture.

One key area of focus for us is evaluating and restricting our own access to customer data. Last summer, we set out to prove that our least-privilege access policies work as intended by applying automated reasoning. Unlike traditional software testing or penetration testing often used in security audits, this method uses mathematical proof that the security properties we intend to protect are always upheld.

We are thrilled to present the results of the work in a paper written by software engineering intern Hye Woong Jeon, a mathematics student at the University of Chicago and Susa Ventures Fellow, who designed and implemented this approach.

Overview of the paper

Stedi’s cloud infrastructure runs on Amazon Web Services (AWS). We use AWS’s Identity Access Management (IAM) Policies at every level of our stack to enable least-privilege access. We grant our engineers and software processes only the minimum necessary permissions required to perform their tasks. Using IAM, we define the specific actions that can be taken on specific resources under specific conditions.

By carefully separating the resources that Stedi needs to make our systems function from customer-owned resources, such as stored data, we can craft access policies that allow us to operate the platform securely while having no access to customer data. IAM independently enforces these access policies – its mechanisms cannot be circumvented. However, this raises a question: how do we know that we have crafted the access control policies correctly? And further, how can we provably demonstrate this not just to ourselves, but also to our customers?

When customers access Stedi’s systems via our API or web UI, they perform actions under their own identity using a specific IAM role that gives them full access to their data – for example, to EDI files stored in Stedi Buckets. When our engineers operate Stedi systems, or our automated processes perform tasks such as deployments, they use a different set of IAM roles. This enables us to manage configuration, deploy software, and access the operational logs and metrics necessary to run our services with the high level of availability that our customers expect.

With a clear separation of roles built on top of a security-first, battle-tested system like IAM, the key concern becomes ensuring that the underlying IAM policies for those roles are written as intended – in other words, ensuring that the role assigned to Stedi employees does not inadvertently include an IAM policy that can potentially allow access to customer data. While we carefully peer-review all software configuration changes with particular attention paid to security policies, we wanted to achieve a higher level of certainty. We wanted to prove definitively to ourselves that we hadn’t made an error, and put in place a mechanism that provides ongoing assurance that our access controls match our intent.

Concrete and complete proof is difficult to come by – especially for the sort of complex systems that Stedi builds – but, given a well-enough defined problem, automated reasoning makes it possible.

Our proof used a Satisfiability Modulo Theory (SMT) solver, a class of logic statement solvers concerned with identifying if some mathematical formula is satisfiable (i.e. is there some combination of values that will make some formula true). Examples of satisfiability questions are not difficult to come by – e.g. if there are twenty apples and oranges, and four more oranges than apples, then how many apples/oranges are there? In this example, twelve oranges and eight apples satisfies the formula.

The problem of access control can also be formulated as a satisfiability problem. For any Stedi-affiliated account X, can X access customer data? A more rigorous characterization of this problem requires understanding the different components that make up the formula of “accessing customer data.”

AWS encodes IAM policies using a specialized JSON grammar, which breaks IAM into several core components: Actions, Principals, Effects, and Resources. In brief, an IAM policy consists of an Effect, which describes if a Principal is allowed to perform an Action on a Resource. These core components hence act as the apples and oranges of our elementary example: under the various combinations of Actions, Principals, Effects, and Resources ascribed to Stedi account X, does there exist some combination that allows X to access a customer account?

Under the well-defined structure of IAM policies, it is relatively straightforward to encode access control for use in the SMT solver. Once each grammar component has been translated into its appropriate logical formulation, encoded policies can be tested against various template policies to check if a policy is allowed to (or prohibited from) accessing customer data.

Our implementation sorted roles into three categories: allowed, prohibited, and inconclusive. We ensured that items in the allowed and prohibited categories were appropriately categorized and invested time in making changes to IAM policies in the inconclusive category to get further assurance that our policies functioned as intended. Overall, we found that using the proof techniques gave us an even higher level of confidence that our security controls work as intended, isolating our own systems from the data our customers have entrusted to us.

More details about the tools and methods we used to conduct this research and our full conclusions are available in the paper.