물리 사기브(Mooly Sagiv)(본명 슈무엘 사기브(Shmuel Sagiv))는 블록체인 분야에서 스마트 컨트랙트의 보안을 강화하기 위해 형식 검증(formal verification)의 적용을 확장하고자 공동 설립한 기업인 세르토라(Certora)의 수석 과학자(Chief Scientist)입니다. ^{[1] [11]}

초기 생애 및 교육

물리 사기브는 이스라엘에서 태어났으며 어린 시절부터 수학과 컴퓨터 과학에 뛰어난 재능을 보였습니다. 그는 테크니온 - 이스라엘 공과대학교(Technion - Israel Institute of Technology)에서 고등 교육을 받았으며, 1991년에 컴퓨터 과학 박사 학위를 취득했습니다. 그의 박사 연구는 소프트웨어 검증 분야에서 향후 그가 이룩할 혁신의 토대가 되었습니다. ^{[2] [11]}

경력

학술 경력

물리 사기브는 텔아비브 대학교에서 강사로 시작해 정교수까지 오르며 학술 경력을 쌓았습니다. 그는 1998년 4월부터 텔아비브 대학교 블라바트닉 컴퓨터 과학 및 AI 학부의 소프트웨어 시스템 석좌교수 및 교수로 재직하고 있으며, 이는 이후 디지털 자산 관련 연구의 기초가 되었습니다.

그의 연구는 프로그램 분석과 소프트웨어 검증에 집중되어 왔습니다. 연구 분야로는 정적 프로그램 분석, 형상 분석(shape analysis), 추상 해석(abstract interpretation), 논리학, 정리 증명, 프로그래밍 언어, 형식 방법론, 데이터 흐름 분석, 프로그램 슬라이싱, 네트워크 검증 및 스마트 컨트랙트 등이 있습니다. 그의 가장 많이 인용된 논문은 3치 논리(three-valued logic)를 통한 형상 분석을 다루고 있으며, 이는 TVLA 시스템으로 구현되었습니다.

사기브의 출판물들은 데이터 흐름 분석, 심볼릭 실행(symbolic execution), 그리고 프로그램 동작을 분석하고 검증하는 데 사용되는 방법론들을 조사합니다. 그의 학술적 작업에는 정리 증명 및 추상 해석과 관련된 연구도 포함되어 있습니다.

2006년 8월부터 2007년 8월까지 사기브는 캘리포니아 대학교 버클리 캠퍼스(UC Berkeley)의 전기공학 및 컴퓨터 과학(EECS) 학과에서 방문 교수로 재직했습니다. 2008년 8월부터 2010년 8월 사이에는 스탠퍼드 대학교에서 방문 연구원으로 활동했습니다.

프로그래밍 언어 연구 커뮤니티 내의 저술 및 협업에 관한 한 연구에서는 사기브를 "PLDI(Programming Language Design and Implementation) 커뮤니티의 케빈 베이컨"이라고 지칭하기도 했습니다.

IBM

사기브는 1990년 10월부터 1993년 10월까지 이스라엘 하이파에 위치한 IBM에서 팀장으로 근무했습니다.

세르토라 (Certora)

2018년, 사기브는 스마트 컨트랙트 및 블록체인 기반 소프트웨어 시스템의 형식 검증에 주력하는 기업인 세르토라를 공동 설립했습니다. 그는 2018년 11월부터 2025년 6월까지 최고 경영자(CEO)를 역임했습니다.

이 회사는 탈중앙화 금융(DeFi) 애플리케이션에 사용되는 스마트 컨트랙트와 소프트웨어 시스템의 동작을 분석하기 위한 검증 도구를 개발했습니다.

2025년 6월, 사기브는 뉴욕 대도시권에 기반을 둔 세르토라의 수석 과학자 역할을 맡았습니다.

회사에서 그의 업무는 블록체인 관련 시스템 및 스마트 컨트랙트에 형식 방법론과 소프트웨어 검증 기술을 적용하는 것을 포함합니다.

협업 및 전문 활동

사기브는 프로그래밍 언어 및 소프트웨어 공학에 관한 공동 연구 프로젝트에 참여해 왔습니다. 그의 작업에는 프로그램 분석 및 소프트웨어 검증과 관련된 협업이 포함됩니다.

그는 또한 유럽 프로그래밍 심포지엄(ESOP) 및 국제 소프트웨어 공학 컨퍼런스(ICSE)를 포함하여 컴퓨터 과학 및 소프트웨어 공학 관련 컨퍼런스와 심포지엄에 참여해 왔습니다.

수상 및 인정

사기브는 1989년 울프 재단 펠로우십(Wolf Foundation Fellowship)을 받았으며, 1993년 IBM 우수 기술 성취상(IBM Outstanding Technical Achievement Award)을 수상했습니다. 2000년에서 2005년 사이에는 IBM 교수진 상(IBM Faculty Awards)을 받았습니다.

2002년에는 프리드리히 빌헬름 베셀 연구상(Friedrich Wilhelm Bessel Research Award)을 수상했습니다.

2011년, 사기브는 토마스 렙스(Thomas Reps), 수잔 호로비츠(Susan Horowitz), 제네비브 로제이(Genevieve Rosay)와 함께 ACM SIGSOFT 회고적 영향력 있는 논문상(Retrospective Impact Paper Award)을 수상했습니다.

2016년에는 마이크로소프트 우수 협력자상(Microsoft Outstanding Collaborator Award)을 받았으며 ACM 펠로우(ACM Fellow)로 선정되었습니다.

소프트웨어 공학, 프로그램 분석 및 형식 방법론 분야에서의 그의 업적은 학술상, 연구 협업, 그리고 학계와 산업계에서의 직책을 통해 인정받고 있습니다. ^{[1] [2] [3] [4] [5] [6] [7] [8] [9] [10] [11]}

인터뷰

핀테크 심포지엄 2019 스마트 컨트랙트 분석 #01

2019년 7월 15일, 물리 사기브는 유튜브 채널 "Datalogisk Institut - Københavns Universitet"에서 주최한 핀테크 심포지엄 2019에서 "스마트 컨트랙트의 정확한 정적 분석을 위한 모듈성"이라는 주제로 기조 연설을 했습니다.

발표 중에 사기브는 배포 전 소프트웨어 취약점을 식별하고 특정 프로그램 속성을 검증하기 위한 기술에 중점을 둔 스마트 컨트랙트 정적 분석 방법론을 논의했습니다. 그는 기존의 일부 산업용 분석 도구들이 분석 정밀도의 한계로 인해 오탐(false positives)을 발생시키거나 특정 오류를 감지하지 못할 수 있다고 언급했습니다.

사기브는 소스 코드가 아닌 이더리움 가상 머신(EVM) 바이트코드에서 작동하는 정확한 정적 분석(ASA)이라 불리는 접근 방식을 설명했습니다. 발표에 따르면, 이 방법은 소스 파일이 없는 경우에도 컨트랙트를 분석할 수 있게 해줍니다.

이 강연에서는 외부 컨트랙트의 예상되는 동작 및 시스템 요구 사항과 관련하여 컨트랙트를 평가하도록 설계된 모듈식 검증 방법도 다루었습니다. 추가적인 주제로는 형식 명세(formal specifications), 재진입성(reentrancy) 취약점, 금융 로직 조건, 그리고 스마트 컨트랙트 개발 워크플로우 내에서의 자동화된 검증 절차 사용 등이 포함되었습니다. ^[12]

ETHGlobal 형식 검증 워크숍 #02

2022년 10월 18일, 물리 사기브는 ETHGlobal 유튜브 채널에서 주최한 "효과적인 코드 보안 도구"라는 제목의 워크숍에 참여했습니다. 세션 동안 그는 기존 감사 및 정적 분석 도구의 오탐 및 미탐 취약점을 포함하여 스마트 컨트랙트 보안 분석과 관련된 과제들을 논의했습니다.

발표에서 사기브는 형식 검증을 스마트 컨트랙트 코드와 예상되는 시스템 동작을 정의하기 위한 수학적 명세를 결합하는 방법으로 설명했습니다. 그는 세르토라의 검증 프레임워크가 컴파일된 EVM 바이트코드를 분석하여 실행 중에 사전 정의된 조건과 불변량(invariants)이 유지되는지 평가한다고 설명했습니다.

워크숍에는 탈중앙화 금융(DeFi) 프로토콜 및 자동화된 마켓 메이커(AMM)와 관련된 예시가 포함되었습니다. 사기브는 명세 기반 검증이 지급 능력 조건, 불변량 위반 및 예외적인 실행 시나리오와 관련된 사례를 식별하는 데 사용될 수 있다고 밝혔습니다. 그는 또한 형식 검증을 수동 감사, 퍼즈 테스팅(fuzz testing) 및 기타 보안 검토 방법과 함께 사용할 수 있는 프로세스로 설명했습니다.

이 세션에서는 소프트웨어 개발 워크플로우에서 형식 명세의 역할에 대해서도 더 깊이 다루었습니다. 사기브는 검증 프로세스가 후기 단계의 감사 중에만 적용되는 것이 아니라 개발 전반에 걸쳐 통합될 때 더 효과적이라고 언급했습니다. ^[13]