现代处理器的分支预测器利用饱和计数器来提升指令级并行性，但传统饱和计数器是确定性的，容易受到侧信道攻击：攻击者可通过操作计数器状态并观察缓存行为（如Prime+Probe）推断受害进程的分支方向。为缓解该泄漏，已有研究提出概率饱和计数器（PSC），通过随机化更新来干扰攻击者的观测，但现有评估主要依赖经验仿真，缺乏严格的安全保证。本文基于差分隐私（DP）对PSC进行形式化分析：将PSC和对应的Prime+Probe攻击策略建模为概率摩尔机，推导攻击者最优观测策略，并利用差分隐私量化攻击者的区分能力。作者证明，所提出的DP保证适用于Prime+Probe观测模型下的PSC原语；而完整分支预测器在重复或自适应攻击下的端到端安全性被列为未来工作。在此基础上，本文为增强型PSC综合参数，使其满足目标纯差分隐私保证，并针对效用指标推导稳态误预测率的闭式表达，随后在基准程序上验证理论预测。实验表明，与确定性饱和计数器及现有概率计数器相比，综合得到的PSC既能提供正式的安全保证，又能保持有竞争力的预测性能。该工作首次将差分隐私形式化方法引入硬件级分支预测器侧信道防御，为微架构安全设计提供了可证明的定量分析框架。适合处理器微架构设计者、硬件安全研究者和形式化方法领域人员阅读。