raytheonbbn/maude-hcs은닉 통신 시스템을 위한 정형 모델링 및 분석 프레임워크로, 은닉 채널, 공격자 모델의 명세와 탐지 불가능성-성능 간 트레이드오프에 대한 통계적 모델 검증을 가능하게 합니다.
Maude-HCS는 실제 규모에서 Hidden Communication Systems (HCS)를 공식적으로 명세하고 추론하기 위한 최초의 일반화되고 모듈화된 툴체인 중 하나입니다. 이를 통해 네트워크 설계자는 대체 HCS 설계를 신속하고 효과적으로 탐색할 수 있으며, 설계를 신뢰하는 데 필요한 공식적인 개인정보 보호 및 성능 보장을 제공합니다.
숨은 통신 시스템(Hidden Communication Systems, HCS)은 일반 네트워크 활동 내에 은밀한 메시지를 삽입하여 통신의 존재를 숨깁니다. 실제로 HCS의 탐지 불가능성은 일반적으로 임시 트래픽 통계나 특정 탐지기를 사용하여 평가되므로, 보안 주장은 실험 설정과 암묵적인 공격자 가정에 밀접하게 연결됩니다.
Maude-HCS는 실행 가능한 모델링 및 분석 프레임워크로, 복잡한 HCS 설계에서 탐지 불가능성-성능 간의 트레이드오프를 추론하기 위한 원칙적이고 실행 가능한 기반을 제공합니다. 설계자는 프로토콜 동작, 공격자 관찰 가능 항목 및 환경 가정을 공식적으로 명세하고, 유도된 추적 분포에서 몬테카를로 샘플을 생성합니다. 이를 사용하여 통계적 검정의 참양성률과 거짓양성률을 추정하고 이러한 추정치를 탐지 불가능성 측정에 대한 하한으로 변환함으로써 탐지 불가능성 주장을 감사할 수 있습니다. 이를 통해 명시적으로 명시된 모델링 가정 하에서 탐지 가능성과 성능 간의 트레이드오프를 체계적으로 평가할 수 있습니다.
HCS 모델링 및 추론에 도움이 필요하시면 저희에게 연락해 주십시오. 그리고 연구의 일환으로 이 작업을 사용하신다면 인용을 고려해 주시기 바랍니다.```bibtex @article{khoury2026maude, title={Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems}, author={Khoury, Joud and Kim, Minyoung and Merlin, Christophe and Meseguer, Jos{'e} and Ratliff, Zachary and Talcott, Carolyn}, journal={arXiv preprint arXiv:2603.03369}, year={2026} }
## 요구 사항
Python 버전 `3.12.4` 필요
선호하는 환경을 만들고 활성화하세요. 예:
pyenv의 경우```bash
pyenv install 3.12.4
pyenv local 3.12.4
conda의 경우```bash conda create --name pwnd2 python=3.12.4 conda activate pwnd2
가상 환경의 경우```bash
python -m venv venv
source venv/bin/activate
저장소 소스 코드는 dns-formalization-maude를 종속성(서브모듈)으로 가져오도록 구조화했습니다. 이 종속성의 포크를 만들어 변경 사항을 추적할 수 있도록 했습니다. 희소 체크아웃(sparse-checkout)을 사용하여 Testbed와 같이 관련 없는 많은 파일이 포함된 종속성의 모든 소스를 체크아웃할 필요가 없도록 했습니다.
메인 저장소를 복제하려면```shell git clone [email protected]:raytheonbbn/maude-hcs.git
메인 브랜치는 최신(불안정할 수 있음) 소스를 포함합니다.
`pwnd.cp1`과 같은 이전 브랜치/태그는 평가 중 결과를 생성하는 데 사용된 안정적인 스냅샷을 나타냅니다
(예: `pwnd.cp1`은 챌린지 문제 1에 사용, `pwnd.cp2`도 동일).
이전 스냅샷을 사용하려면 특정 브랜치(예: `pwnd.cp1`)를 체크아웃하세요.
코드 복제본을 사용하여 dns 서브모듈을 설정하여 원본 소스의 변경 사항을 추적할 수 있도록 하고,
sparse-checkout을 사용하여 관련 소스만 유지하세요.```shell
cd maude-hcs
mkdir -p maude_hcs/deps
git submodule add -b <branch> -f [email protected]:raytheonbbn/dns-formalization-maude.git \
maude_hcs/deps/dns_formalization
cd maude_hcs/deps/dns_formalization
git sparse-checkout init --cone
git sparse-checkout set "Maude/dns" "Maude/common" "Maude/test" "Maude/attack_exploration"
cd ../../../
git reset .gitmodules
git reset maude_hcs/deps/dns_formalization
위 명령에서 <branch>를 pwnd.43.rb1로 설정하면 챌린지 문제 1의 결과를 재현할 수 있고, pwnd로 설정하면 최신 버전을 사용할 수 있습니다.
위 작업은 sparse-checkout 파일을 다음 경로에 생성합니다:
.git/modules/maude_hcs/deps/dns_formalization/info/
그리고 해당 파일은 Maude/src와 같은 특정 디렉터리만 포함하도록 지시합니다.
이 시점에서 git status는 깨끗한 시작 상태를 보여야 합니다.
설치하려면 먼저 dns라는 패키지로 종속성을 설치합니다. 이 패키지는 Maude.*로 임포트합니다.
그런 다음 maude_hcs를 패키지로 설치합니다 (dns에 종속됨).```shell
cd maude_hcs/deps/dns_formalization
pip install -e .
cd ../../../
pip install -e .
## 사용자 모델 자동 생성
사용자 모델은 사용자 행동을 나타내기 위한 마르코프 모델입니다.
이는 json 형식으로 제공됩니다.
첫 번째 단계는 이를 공식적인 maude 표현으로 변환하는 것입니다.
이를 위해 다음을 지정하십시오.
- 프로토콜: dns 또는 mastodon
- 변환하려는 모든 json 모델이 포함된 입력 디렉토리
- 모든 json 모델의 maude 버전을 포함할 출력 디렉토리
예를 들어,```shell
# convert dns tgen user models
maude-hcs --verbose \
--protocol=dns markov \
--json-dir=../pwnd-cp2/src/static/tgen_models/dns/ \
--maude-dir=./maude_hcs/lib/tgen/maude/dnsprofiles/markov/
# convert mastodon tgen models
maude-hcs --verbose \
--protocol=mastodon markov \
--json-dir=../pwnd-cp2/src/static/tgen_models/mastodon \
--maude-dir="./maude_hcs/lib/raceboat/maude/mastodonprofiles/"
아래 ./maude_hcs/lib/tgen/maude/dnsprofiles/markov/에서 마르코프 JSON 사양 예제를 확인하세요 (마스토돈도 유사함), 그리고 변환된 마우드 사양도 함께 확인하세요.
generate 명령을 사용하여 초기 구성을 생성합니다.
HCS 구성은 HCS 구성 매개변수를 사용하여 JSON으로 직접 전달하거나, Shadow 실험 구성 파일을 사용하거나, YML 구성 파일을 사용하여 전달할 수 있습니다. 각각에 대해서는 다음에 설명합니다.
다음과 같이 maude-hcs JSON 구성 파일을 전달합니다.
iodine을 사용하여 확률적 DNS 모델 구성을 생성하고 출력 파일 이름을 지정하려면,```shell
maude-hcs --verbose generate
--run-args="./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1-hcsconfig.json"
--model=prob
--filename="cp2_scenario_1"
--output-dir="./use-cases/challenge-problem-2/cp2_scenarios/"
`--model=nondet`를 설정하여 비결정론적 버전을 생성합니다.
이렇게 하면 출력 디렉토리에 실행 가능한 maude 파일(및 해당 HCS 구성 json)이 생성됩니다.
입력 json 구성 파일은 따라하기 쉬워야 합니다. 여기에는 다음 사양이 포함됩니다.
* 네트워크 토폴로지(링크 및 해당 특성)
* 적대자(이 경우 zeek 탐지기 프로필, 이동 평균 탐지기의 기준 데이터 및 해당 구성)
* 채널/프로토콜: 각 프로토콜에는 이상한 네트워크와 기본 네트워크 프로토콜이 포함됩니다. 전자는 후자에 데이터를 숨기거나 삽입합니다. 예를 들어, Iodine은 DNS에 삽입되므로(따라서 채널 이름은 iodine-dns) Destini는 Mastodon에 삽입됩니다.
일부 매개변수에 대한 설명은 [HCSParamsGuide](https://github.com/raytheonbbn/maude-hcs/blob/main/HCSParamsGuide.md)를 참조하세요.
확률적 모델은 비결정론적 매개변수뿐만 아니라 확률적 매개변수(비결정론적 매개변수를 재정의함)도 결합합니다.
### YML 구성 사용
#### 단일 구성
YML 구성에는 터널 및 기본 네트워크의 전체 구성이 포함됩니다.
여기서 직접 HCS 구성을 생성할 수 있습니다.```shell
maude-hcs --verbose generate --yml-filename=./use-cases/challenge-problem-2/cp2_setup_example.yml --model=prob --filename=generated_test_yml
CP2와 같은 배치 구성의 경우, 여러 YML 파일을 Maude 시나리오 파일로 변환하십시오:```shell ./scripts/generate_cp2_maude.sh [scenario_dir]
여기서 `scenario_dir`은 선택 사항입니다(기본값: `../pwnd_cp2`)
### Shadow yaml 구성 사용하기
네트워크 구성은 HCS config json 대신 shadow 파일을 사용하여 지정할 수 있습니다.
(Shadow 시뮬레이터에 대한 자세한 내용은 [Shadow](https://github.com/shadow/shadow)를 참조하십시오.)
shadow 파일에 정의된 특성을 사용하는 모델을 생성하려면 다음을 지정하십시오:```shell
--shadow-filename <path_to_shadow_file.yaml>
shadow yaml 파일은 네트워크, 호스트 및 프로세스 구성을 지정합니다.
shadow 네트워크 구성이 ../pwnd-cp1 디렉토리에 있다고 가정하고, 실행하십시오.```shell
maude-hcs --verbose --protocol=dns generate --shadow-filename=../pwnd-cp1/shadow_files/examples/cp1_sim_config.yaml --model=prob --filename=generated_test_shadow
## HCS 구성 실행
### Maude로 독립 실행
독립 실행형 maude에서 구성을 실행하려면 먼저 시스템에 [standalone maude](https://github.com/maude-lang/Maude)를 설치하세요(버전 3.5.0 이하를 권장합니다).
단일 구성을 실행하려면 파일 이름과 함께 maude를 호출합니다. 예를 들어, `results`에서,```shell
maude ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude
Maude 프롬프트 안에서, 다음을 입력하세요```shell rew initConfig .
그러면 더 이상 규칙을 찾을 수 없고 더 이상 진행할 수 없을 때까지 모든 재작성을 실행합니다.
로깅을 추가하면 실행의 장황함이 함께 증가합니다.```shell
set print attribute on .
실행은 다음 명령어를 통해 단계별로 진행할 수도 있습니다 (maude 매뉴얼 참조)```shell rew[1] initConfig . cont 1 .
### 통계적 모델 검사
통계적 모델 검사는 [QMaude](https://github.com/fadoss/umaudemc)의 scheck 하위 명령을 통해 사용할 수 있습니다.```shell
maude-hcs scheck [-h] [--advise]
[--protocol {dns}] [--file FILE] [--test TEST] [--initial INITIAL] [--query QUERY]
[--assign METHOD] [--alpha ALPHA] [--delta DELTA]
[--seed SEED] [--jobs JOBS] [--format {text,json}]