thomasarmel/rollback_car_attack_proverif차량 키폡의 롤백 공격에 대한 ProVerif 개념 증명 (CVE-2022-37418, CVE-2022-36945 및 CVE-2022-37305)
자동차 키폰에 대한 롤백 공격의 ProVerif 개념 증명 (CVE-2022-37418, CVE-2022-36945, CVE-2022-37305), [1]에 발표됨
저자는 [1]의 저자들과 아무런 관련이 없습니다. 논문을 오픈 액세스로 제공해 주신 것에 감사드립니다.
ProVerif 형식 검증 PoC를 실행하려면 먼저 공식 페이지의 지침에 따라 ProVerif을 설치하세요.
또는 amd64 아키텍처의 Linux용 정적 바이너리를 사전 컴파일하여 저장소의 릴리스 페이지에서 제공합니다. Windows용 실행 파일도 있습니다.
다운로드한 실행 파일에 실행 권한을 추가해야 합니다:
chmod +x proverif_linux_amd64_static
git clone https://github.com/thomasarmel/rollback_car_attack_proverif.git
cd rollback_car_attack_proverif/
proverif model.pv
자동차가 열려도 키폰이 눌렸음을 의미하지 않는다는 것을 볼 수 있습니다. 즉, 공격자가 자동차 열기에 성공했다는 뜻입니다:
정확히, 이 쿼리는 키폰을 누른 횟수보다 더 많은 횟수로 열림 메커니즘을 트리거할 수 있음을 의미합니다.
다음 쿼리가
inj-event(car_open) ==> inj-event(fob_pressed)
false를 반환하는 반면, Proverif은 다음 쿼리
event(car_open) ==> event(fob_pressed)
는 true를 반환했을 것이라고 알려줍니다:
이는 자동차를 열려면 키폰을 눌러야 하지만, 키폰을 누른 횟수보다 더 많은 횟수로 자동차를 열 수 있음을 의미합니다.
추적 PDF를 생성하려면 ProVerif에 Graphviz가 설치되어 있고 PATH 환경 변수에 추가되어 있어야 합니다.
Linux에서는 다음을 사용하여 설치할 수 있습니다:
sudo apt update
sudo apt install graphviz
Windows에서는 https://graphviz.org/download/ 에서 설치 프로그램을 다운로드할 수 있습니다. 설치 폴더를 PATH 환경 변수에 추가해야 합니다:
공격을 상세히 설명하는 그래프를 생성하려면 다음을 실행하세요:
proverif -graph . model.pv
이제 생성된 PDF 파일을 열어 공격자가 키폰을 누르지 않고도 자동차 열림을 어떻게 트리거할 수 있는지 확인하세요:
[1] Csikor, Levente and Lim, Hoon Wei and Wong, Jun Wen and Ramesh, Soundarya and Parameswarath, Rohini Poolat and Chan, Mun Choon, Rollback: A new time-agnostic replay attack against the automotive remote keyless entry systems, ACM Transactions on Cyber-Physical Systems, 2024, https://doi.org/10.1145/3627827