网络协议分析和验证

先修要求

• 计算机网络和应用密码学基础。
• 理解状态机、逻辑和基本程序分析。
• 能够编写测试 harness 或协议脚本。

学习目标

• 从规范和流量中抽取协议状态机。
• 编写协议解析、模糊测试和一致性测试工具。
• 用模型检查或符号工具验证关键性质。
• 识别认证、重放、降级和状态混淆问题。
• 把验证结果转化为工程修复建议。

教学组织

• 每周 2 次课堂：一次讲授核心概念，一次用于实验、论文讨论或项目评审。
• 课程按 16 周推进，每周都有可检查的作业、实验或项目里程碑。
• 强调可复现材料：代码、配置、数据、实验日志和报告需要能被助教或同学复查。

周计划

考核方式

课程项目

项目选择一个真实或教学协议，完成状态机建模、测试工具、性质验证和安全评估。

课程政策

• 允许使用 AI 工具，但所有生成代码、实验记录和设计建议必须经过学生本人审查，并在报告中说明使用方式。
• 严禁提交不能解释的代码、证明、配置或实验结果；答辩时每名成员都需要解释自己负责部分的设计、测试和取舍。
• 迟交会影响迭代评分，但课程更看重可复现、可审计和可维护的结果，而不是临时堆砌。