Amazon Web Services (AWS) open sourced its Cedar policy language and software development kit (SDK), which is unique because it was designed around automated reasoning, according to AWS Director of Open Source Marketing David Nalley.

The Cedar language, which was initially created by AWS to run under the hood of its Amazon Verified Permissions and AWS Verified Access managed services, allows developers to abstract away authorization from the rest of the application and "verify that what you think you have codified in policy is what reality is going to be when the application is running," Nalley told SDxCentral.

The capability of automated reasoning to confirm that "what you think you've done is actually what you've done is incredibly powerful" and "allows folks to have much greater assurance," Nalley said. Automated reasoning also renders "double and triple checking [policies or code] very easy" because Cedar was designed "from the ground up" with that approach plugged in, he noted.

Nalley described automated reasoning as the concept that rather than working out every possible combination by hand, "we can look at mathematical proofs and use the idea of math that has already been proven ... and apply that to computer science."

For example, instead of plugging in and checking every integer in a program or application, automated reasoning looks at how to logically prove something will or will not work.

And while that doesn't always reveal a solution, "that highlights a problem in itself," Nalley said. "We look for that logic to say that we can definitely prove something, that we can definitely disprove something or we're not sure. That essentially allows us to either have confidence that we know what something's going to do," or "we have confidence that something is not going to behave in a specific way," he said.

That flow of logic "gives us a pointer of where we need to spend more time or spend less time because we can establish that one way or the other," he added, citing automated reasoning as "an area of the science behind computing that does not get enough attention."

Humans are known for making a good deal of mistakes, so "when we can add assurance to how we think about software and how we think about logic flow within software that we're writing, that's incredibly compelling," Nalley said. "We can add a lot of functionality around assurance of what we think of programs actually going to do."

The decision to open source both the Cedar language and SDK is based on transparency, according to AWS.

"We want people to be able to inspect what we're doing in terms of Amazon Verified Access and Amazon Verified Permissions so they have confidence in how that works," Nalley said. "We welcome other people to come participate with us, but mainly we want to make this available as another tool that folks can use to help build greater assurance into their own applications."