Formal은 장기 자격 증명을 건네지 않고도 클라우드 코딩 에이전트가 운영 데이터와 인프라에 접근하도록 하는 방식을 소개했다. OpenID Connect(OIDC)를 이용해 에이전트 실행마다 별도 신원을 부여하고, 사람의 승인과 정책에 따라 접근을 제한하는 방식이다.

Formal의 OIDC 통합은 머신 워크로드가 자체 인프라 신원을 증명하도록 한다. 워크로드는 ID 제공자(IdP)에서 단기 토큰을 받아 서비스에 전달하고, 서비스는 공개 키와 토큰의 서명·클레임을 확인한다. Formal에서는 고객이 통합별 CEL 조건을 설정해 인증을 제한할 수 있으며, OIDC 클레임을 권한 설정에도 활용할 수 있다.

OIDC 인증을 거친 호출자는 CreateFederationToken으로 단기 Connector 접근 토큰을 받을 수 있다. 토큰에는 원래 OIDC 토큰의 클레임이 포함되므로, 워크로드는 장기 자격 증명을 저장하지 않고 Connector를 자격 증명 전달 프록시로 사용할 수 있다. SPIRE의 JWT-SVID도 OIDC 토큰처럼 검증하며, SPIFFE ID를 정책과 권한 설정에 사용할 수 있다. OIDC는 Formal Endpoint와 Kubernetes Egress Agent 인증에도 쓰인다.

통합은 머신 신원 하나에 연결되지만, 필요하면 토큰의 클레임에서 사람의 신원을 확인하도록 설정할 수도 있다. Formal은 머신 신원을 암호학적으로 확인하지만, 사람 신원은 연결된 워크로드가 주장하는 값이다. 고객이 해당 시스템을 신뢰하고 Formal에 그 값을 신뢰하도록 설정한 경우 이를 받아들인다. Formal은 Metabase 같은 BI 도구에서 데이터베이스 요청에 최종 사용자 신원을 전달하던 방식도 클라우드 에이전트 접근 통제에 적용할 수 있다고 설명한다.

Formal은 자사 제품을 내부에서 사용해 운영 데이터베이스, S3 버킷, 로그 클러스터 앞에 Connector를 두고, 개발자 노트북에서 코딩 에이전트 사용을 감시·통제한다고 밝혔다. Terraform Cloud가 Formal 제어 평면에 인증할 때 장기 API 키 대신 OIDC를 쓰도록 바꾼 것도 내부 적용 사례다.

운영 데이터베이스를 이용하는 제품 분석에서는 에이전트가 데이터베이스 접근을 요청하고, 사람이 Slack에서 이유와 기간을 확인해 승인할 수 있다. 승인된 접근은 해당 에이전트 세션과 요청한 데이터베이스로 제한된다. 비동기 워크플로를 조사할 때도 에이전트가 단기 접근을 요청할 수 있으며, 요청은 Formal에 기록되고 에이전트와 실행을 시작한 엔지니어 모두에게 귀속된다.

개발 환경에서는 에이전트가 OIDC로 Formal 개발 테넌트와 클라우드 제공업체의 개발 계정에 접근해 실제 환경에서 변경 사항을 확인할 수 있다. Formal은 사례로 Cursor 클라우드 에이전트가 개발용 Azure 계정에 AKS 클러스터를 배포하고, PR 브랜치의 Kubernetes 오퍼레이터를 실행해 FormalPolicy CRD가 개발 테넌트에 동기화되는지 확인한 일을 들었다.

Formal은 운영 환경 접근은 읽기 전용이며 사람의 승인을 거치도록 하고, 개발 환경에서는 더 넓은 권한을 부여할 수 있다고 설명한다. 다만 이 방식에서도 사람 신원은 워크로드가 제공하는 클레임에 의존한다. 회사는 에이전트 접근을 장기 자격 증명으로 처리하기보다, 실행별로 범위가 정해진 임시 위임으로 다루는 것이 내부 활용에서 얻은 교훈이라고 밝혔다.