search

smithy-lang / smithy-dafny

Apache License 2.0
9 stars 8 forks source link

Model Access Denied from AWS Services #609

Open texastony opened 4 days ago

texastony commented 4 days ago

User Story

As a Smithy-Dafny customer I want Smithy-Dafny to model access denied errors from AWS Services so I can implement Dafny logic to handle such access denied errors.

Current State

It appears that MOST access denied errors from AWS Services are not formally modeled in the Smithy Models that Crypto Tools and presumably other Smithy-Dafny customers have been using to model AWS Services such as KMS.

Thus, these access denied errors are turned into "opaque" objects.

Crypto Tools and other Smithy-Dafny customers cannot process opaque errors in Dafny, as they hold entirely generic/unspecified object:

| Opaque(obj: object)

This may be a Smithy flaw, or a flaw in how AWS Smithy Models are processed by Smithy-Dafny.

Partial Mitigations

At the very least, representing the message/string component of the access denied error, along with the generic object, would allow Smithy-Dafny customers to execute string parsing in Dafny on the access denied error.

If we can differentiate between a truly opaque error (i.e: any arbitrary exception thrown, such as Heap Exhaustion, or Kernel Panic) and an access denied exception, that is significant and possibly even sufficient progress on this matter.

robin-aws commented 2 days ago

This is a generic Smithy gap: there are errors that could be modeled that are a result of platform error cases, such as access denied because of the authentication mechanism necessary to call an AWS service. It affects codegen for AWS SDKs as well and there are some internal proposals for solutions already - I'll dig them up and reach out to you.

robin-aws commented 17 hours ago

Rather than falling back to error message parsing (which is naturally brittle and would have to be replicated slightly differently across languages), I suggest we just expose the status code from any SDK error. All AWS SDKs should make this available as the fallback information to react to for unmodeled errors, e.g. the comment on Rust's Unhandled here: https://docs.rs/aws-sdk-kms/latest/aws_sdk_kms/enum.Error.html#variant.Unhandled

Exact design to be bike-shedded, but as a strawperson proposal we could just add an additional statusCode: int32 member to the Opaque data constructor of Dafny's Error type for SDK projects.

texastony commented 16 hours ago

I need to parse the string.

Why can't we do both?