ITPE * JackerLab

개요Cedar는 AWS Verified Permissions 및 Amazon Verified Access와 같은 서비스에서 사용되는 정책 언어(Policy Language)로, 권한 관리(Authorization)와 접근 제어(Access Control)를 안전하고 투명하게 정의하기 위해 개발된 오픈소스 언어이다. 개발자는 Cedar를 통해 세밀한 정책 기반 접근 제어(Fine-Grained Authorization) 를 선언적으로 구현할 수 있다.1. 개념 및 정의항목내용비교개념접근 권한을 명시적으로 정의하는 정책 언어JSON 기반 IAM Policy의 대체 혹은 보완목적안전하고 명확한 접근 제어 로직 제공애플리케이션 레벨 접근 통제 구현필요성정책 오작동 및 권한 남용 방지보안 감사 및 검증 자동화2...

개요탈중앙화 금융(DeFi)은 코드로 구현된 스마트 계약을 통해 자산 교환, 대출, 파생상품 등 복잡한 금융 로직을 자동 실행합니다. 하지만 코드 오류나 취약점은 수백억 원에 달하는 피해로 이어질 수 있습니다. 이를 해결하기 위한 핵심 기법이 바로 **Formal Verification(형식 검증)**입니다. 이는 스마트 계약을 수학적 모델로 추상화하고, 사전에 정의된 보안·기능 요구사항을 논리적으로 증명하는 과정으로, DeFi 생태계의 신뢰성과 안전성을 높이는 데 필수적인 기술입니다.1. 개념 및 정의Formal Verification은 소프트웨어나 스마트 계약의 동작을 수학적으로 모델링하고, 논리 기반의 자동화된 증명 도구를 사용해 오류 가능성을 완전히 제거하는 검증 기법입니다. 스마트 계약의 로직을..