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/HEAD/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}]
options:
--help, -h Show help message and exit
--advise Do not suppress debug messages from Maude
--protocol PR The protocol module being analyzed e.g., dns, which points to an smc file specific to that protocol.
--file FILE Maude source file specifying the model-checking problem. If --protocol is specified, this parameter becomes optional, and if specified overrides the protocol smc file.
--test TEST Test generated from maude-hcs, default=results/generated_test.maude
--initial INITIAL Initial term, default=initConfig
--query QUERY QuaTEx query, default=smc/query.quatex
--assign METHOD Assign probabilities to the successors according to the given method, default=pmaude
--alpha ALPHA, -a ALPHA Required significance level for the confidence interval, default=0.05
--delta DELTA, -d DELTA Maximum admissible radius for the confidence interval around the mean, default=0.5
--seed SEED, -s SEED Random seed
--jobs JOBS, -j JOBS Number of parallel simulation threads, default=1, -j 0 will start as many jobs as CPU units
--format {text,json} Output format for the simulation results, default=text
--distribute WORKERS Distribute the computation across multiple machines, specified as a list of workers for the simulation.
--dump OUTPUTFILE Dump query evaluations into the given file. Currently, it only works with the sequential version (-j 1).
For each simulation, a line is written with the result of all queries separated by space.
-D D Define a constant to be used in QuaTEx expressions.
위 명령어로 생성된 파일에 대한 예시 SMC 실행은 다음과 같습니다:```shell maude-hcs scheck --test ./use-cases/challenge-problem-2/cp2_scenarios/cp2_scenario_1.maude --query ./smc/cp2_eval_cp2_scenario_1.quatex -j 0 -n 30-120
확률적 모델과 초기 구성은 Maude로 지정되어야 하며, ``--test TEST`` 옵션(기본값: ``results/generated_test.maude``)을 통해 제공되어야 합니다.
Maude 실행은 ``--initail INITIAL`` 옵션(기본값: ``TEST``에 지정된 ``initConfig``)을 통해 제공된 초기 항(term)에서 시작하여 최종 구성(final configuration)으로 재작성(rewrite)됩니다.
최종 구성에서, 관찰 가능 값(observables)은 모델 검사 문제를 위한 Maude 소스 파일에 지정된 모니터(monitor)와 적(adversary) 액터를 사용하여 추출됩니다. 이 파일은 ``--file FILE`` 옵션이나 ``--protocol PR`` 옵션을 통해 제공됩니다.
예를 들어 ``--protocol dns``는 `lib/` 아래에 dns 프로토콜을 위해 특별히 생성된 모델 검사 파일을 의미합니다.
평균 지연 시간의 기대값과 같은 정량적 속성(quantitative properties)은 QuaTEx 수식을 사용하여 지정하고 ``--query QUERY`` 옵션(기본값: ``smc/query.quatex``)을 통해 제공할 수 있습니다.
유출된 파일을 기준으로 한 저희 예시의 지연 시간 및 확장성 메트릭(metrics)은 ``smc/latency.quatex``와 ``smc/scalability_cp2_scenario_1.quatex``에 정의되어 있으며, ``smc/cp2_eval_cp2_scenario_1.quatex``로 임포트(import)되고, 다음과 같은 형태의 QuaTEx 수식으로 표현될 수 있습니다:```shell
Latency() = s.rval("getLatency(getMonitor(C))");
eval E[Latency()] with delta = 2;
ExfilFilesC2() =
if (s.rval("getToDCumulativeNQueryPostNAT(C,416)") == 0.0) then
discard
else
s.rval("getExfilFiles(getMonitor(C), getToDCumulativeNQueryPostNAT(C,416))")
fi;
eval E[ExfilFilesC2()];
여기서 Latency() 표현식은 모니터에서 지연 시간 값을 추출하고 delta = 2로 기댓값을 평가합니다.
ExfilFilesC2() 표현식은 조건부로 유출된 파일 수를 평가합니다:
만약 사후 NAT DNS 쿼리의 누적 수를 기반으로 한 탐지 시간이 0이라면 — 즉, 누적 쿼리 수가 임계값(예: 위 예제의 416)을 초과하지 않아 탐지가 발생하지 않음을 의미 — 해당 샘플은 폐기됩니다.
그렇지 않으면, 탐지 시점까지 유출된 파일 수가 평가됩니다.
샘플링은 지정된 샘플 수(예: -n 30-300과 같은 -n min-max 옵션)에 도달하거나 모든 쿼리가 원하는 통계적 유의성으로 응답될 때까지 계속됩니다.
아래 예제에서 두 번째 쿼리는 기본값 alpha=0.05 및 delta=0.5를 사용하여 30개 샘플 후에 응답되는 반면, 첫 번째 쿼리는 위에서 지정한 대로 with delta = 2를 사용하여 270개 샘플 후에 응답됩니다.
출력에는 다음이 포함됩니다:
위 QuaTEx 공식의 임계값을 500으로 수정하면 일부 샘플이 폐기됩니다.
그런 다음 결과는 폐기된 샘플 수와 함께 보고되며, 통계적 보장은 아래와 같이 나머지 샘플을 사용하여 계산됩니다.```shell
Number of simulations = 270
Query 1 (./smc/readme.quatex:7:1)
μ = 191.80187664851906 σ = 16.429217228790975 r = 1.9685272804723886
Query 2 (./smc/readme.quatex:8:1) (39 simulations)
μ = 9.76923076923077 σ = 0.48458003855418535 r = 0.1570826767676969
where 21 executions out of 60 (35.0%) have been discarded
동일한 병렬화 설정(즉, -j의 동일한 값) 내에서 동일한 실험을 재현하려면, 동일한 무작위 시드와 함께 --seed 옵션을 사용하십시오.
기본적으로 또는 ‑1을 전달할 때는 현재 시간이 시드로 사용됩니다.```shell
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301530777180123 σ = 3.9683630959745835e-05 r = 1.481811132921282e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
Number of simulations = 30 μ = 1.5301436629475402 σ = 5.0836982397393854e-05 r = 1.8982841201450367e-05
### 테스트 자동화
runexp.sh는 생성과 SMC 분석을 결합한 자동화 스크립트입니다. 두 개의 필수 인수를 사용합니다:```shell
runexp.sh CONFIG_FILENAME METRIC
where
CONFIG_FILENAME is the name of the .yaml shadow file defining the experiment
METRIC is the quatex property and can be latency, throughput, goodput, or all
SMC는 머신의 모든 코어를 사용하여 높은 병렬화가 가능하며, 위에서 언급한 -j 0 옵션을 사용하여 몬테카를로 샘플링에서 거의 선형적인 속도 향상을 얻을 수 있습니다.
QMaude는 분산 SMC를 사용하여 머신 간에 더 많은 병렬성을 허용합니다 (이 기능은 아직 활성 테스트 중입니다).
분산 SMC를 실행하려면 하나 이상의 워커가 다음과 같이 시작되어야 합니다.
$ umaudemc sworker -a 127.0.0.1 -p 1234
👂 127.0.0.1:1234에서 수신 대기 중...
새로운 sworker 명령의 유일한 옵션은 주소(-a)와 포트(-p)입니다. 컨트롤러로부터의 연결을 계속 기다립니다.
컨트롤러 측에서는 일반적인 scheck 명령에 --distribute 옵션을 추가하여 실행할 수 있습니다. 예를 들어,
$ maude-hcs scheck --distribute workers.json
workers.json 파일 (TOML 또는 YAML도 가능)은 시뮬레이션을 위한 워커 목록을 지정합니다. 이 파일은 workers 키를 포함하는 딕셔너리여야 하며, 값은 { "workers": [ {"address": "127.0.0.1", "port": 1234} ] } 또는 간단히 { "workers": [ "127.0.0.1:1234" ] } 형태의 목록입니다. 그 외에는 옵션과 출력이 일반적인 scheck 명령과 동일해야 합니다.
scheck 명령은 원격 워커에 연결하여 필요한 모든 정보를 전달하고, 워커를 활성화하며, 지정된 신뢰 수준에 도달할 때까지 결과를 처리합니다. 각 워커가 실행되는 모든 머신에 파일을 수동으로 복사하는 대신, 파일은 연결을 통해 전송됩니다. Maude 포함 항목이 해결되고 평면화된 버전의 Maude 소스가 전송됩니다.
QMaude는 동일한 형식의 모델에 대한 통계적 모델 검사(SMC)를 제공합니다.
latency.quatex와 smc.maude를 실험 디렉토리에 복사하거나 (또는 results에 유지)합니다.
전자를 수정하여 대상 (확률적) 실험을 로드합니다.
실행```shell
umaudemc --no-advise scheck smc initConfig latency.quatex -a 0.05 --assign pmaude -j 50
QMaude는 quatex 쿼리(μ)에 대한 예상 값을 반환하며, 해당 값에 도달하는 데 걸린 Monte Carlo 시뮬레이션 횟수를 반환합니다.
## Tests
테스트를 실행하려면 먼저 환경에 pytest를 설치하세요.```
pip install -e .[test]
그런 다음 단위 테스트를 실행하세요.``` python -m pytest
## 기타 유틸리티
실험에 사용된 JSON 메타데이터 파일로 이미지 디렉토리를 변환하려면,
예를 들어 mastodon tgen 클라이언트가 사용하는 이미지를 생성하려면 (destini의 커버 이미지도 유사함)```shell
maude-hcs --verbose --protocol dnsmastodon images --image-dir ../pwnd-cp2/src/static/images/ --image-out-dir results/
plotfinal.py를 인수 smc_directory, tne_directory, quatex_directory와 함께 사용하세요.```shell
python scripts/plotfinal.py use-cases/challenge-problem-2/results-aligned/ use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/ smc/
동일한 스크립트가 CDF 플롯을 생성합니다.```shell
python scripts/gather\_samples.py use-cases/challenge-problem-2/results-aligned/samples/ use-cases/challenge-problem-2/results-aligned/cdfs use-cases/challenge-problem-2/cp2_scenarios_tne/cp2_te_results/
다음 프로젝트들은 Maude-HCS에서 직접 사용됩니다.