Model Access Denied from AWS Services

[texastony]

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]

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]

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]

I need to parse the string.

Why can't we do both?

[texastony]

@ajewellamz Has started this via #617