lean-sudo가 권한 판단을 증명한 sudo 대체품을 내놨다

lean-sudo는 Ubuntu에서 기존 sudo를 대체하도록 만든 도구다. 권한·정책 판단을 Lean 4로 구현하고 정리를 통해 검증했다고 밝히며, 기존 sudoers 설정과 PAM을 사용한다. 제작자는 이를 보안 판단을 코드 검토에만 맡기지 않는 대안으로 소개한다. lean-sudo 저장소와 설치 안내

도구는 정책 평가, 환경 구성, 명령 인자 처리 등을 순수 Lean으로 작성한 검증 코어와 운영체제 작업을 맡는 셸로 나눈다. 제작자에 따르면 저장소에는 직접 작성한 정리 498개가 있고, 자동 검사에서 Lean의 표준 공리 세 가지 외의 공리를 사용하지 않는 것으로 확인됐다. 다만 정리는 명세를 코드가 따르는지를 보장할 뿐, 명세 자체가 올바른지는 보장하지 않는다.

Ubuntu 26.04 컨테이너에서 실행한 엔드투엔드 테스트에서는 기존 sudo와 각각 sudo 테스트 1113개, visudo 테스트 193개를 통과했다. 무작위 조건을 생성해 두 구현을 비교한 시험에서도 문서화된 차이를 제외하면 차이가 없었다고 프로젝트는 설명한다. 별도 sudo-rs 호환성 테스트에서는 기존 sudo가 861개 중 851개, lean-sudo가 827개를 통과했으며, 기존 sudo는 통과하고 lean-sudo는 통과하지 못한 26개 항목을 차이로 문서화했다. 통합 테스트 안내

두 구현의 동작이 완전히 같지는 않다. lean-sudo는 정책 파일의 구문 오류, 정의되지 않은 별칭, 안전하지 않은 포함 파일 등을 발견하면 부분 정책으로 계속 실행하지 않고 거부한다. 반면 기존 sudo는 일부 상황에서 경고 후 처리 가능한 규칙을 계속 사용한다. 또 lean-sudo는 유효하지 않은 UTF-8 명령행 인자를 거부하고, 미래 시각이 기록된 인증 캐시는 인정하지 않는다.

형식 검증이 시스템 전체를 증명하는 것은 아니다. 프로젝트가 신뢰 대상으로 남겨 둔 항목에는 시스템 호출을 수행하는 C 코드, 검증 코어에 사실을 전달하고 결정을 실행하는 Lean 셸, Lean 커널·컴파일러·런타임과 운영체제가 포함된다. 문서도 증명은 코드가 명세를 따르는지 확인할 뿐, 명세가 sudo의 올바른 동작을 정의하는지는 별도로 살펴야 한다고 밝힌다. 설계와 검증 범위

프로젝트는 아직 새 소프트웨어이며 root 권한을 다룬다고 경고한다. Ubuntu 26.04에서 시험하기 전에 가상 머신이나 컨테이너를 사용하고, 전환 중에는 root 셸을 열어 두며, 기존 sudo 구현을 대체 수단으로 남겨 두라고 안내한다. 기존 /etc/sudoers, /etc/sudoers.d, /etc/sudo.conf와 PAM 설정을 재사용하며, 설치·전환 절차는 저장소에 공개돼 있다.