互联网技术的迅速发展,让现代社会的信息量爆炸式增长。现在人们越来越喜欢在互联网上分享信息,社交网络(Social Network,SN)的出现为数十亿网民提供了快速分享信息的平台。近几年,智能移动设备的普及更加促进了SN的迅猛发展,人们可以通过移动设备随时随地社交和办公,在生活和工作中越来越依赖于SN,国内外热门社交平台的用户数达到了数十亿。庞大用户的数据量使SN成为了网络攻击的重灾区,隐私泄露事件近年来层出不穷,一旦隐私发生泄露,往往涉及大规模的用户,因此SN的安全是不容忽视的。导致隐私泄露原因一方面是SN系统本身的安全性和可靠性不够高,另一方面是用户对自身隐私保护的意识不够强。SN作为一个软件系统,可以用软件验证的方法来提高其安全性和可靠性。然而,传统的软件验证方法比如模型检测、定理证明和测试对于验证复杂的系统存在一些不足。因此,为了提高SN系统的可靠性和安全性,需要采用一种较完善且具备实时性的验证方法。为了验证SN系统,本文提出了一种在线的运行时验证方法。该方法利用源代码插桩技术捕获系统运行时产生的信息,在不需要对系统进行建模的情况下进行实时的验证。首先,获取SN系统的安全相关性质,并用三值命题投影时序逻辑(Three-valued Propositional Projection Temporal Logic,PPTL3)公式形式化描述,再转换为对应的有限状态自动机(性质监控器)。然后,根据系统安全性质中的相关事件确定探针的插桩位置,探针捕获安全性质相关的事件序列,并发送至运行时监控器的接收服务器。同时,运行时监控器读入性质监控器的信息后开始监控系统,实时接收代码探针发送的事件序列并转换为原子命题的组合,性质监控器根据该组合确定每一步的状态转移:当到达接受结点(TRUE或FALSE)时,运行时监控器即停止监控并给出验证结果,否则验证结果为inconclusive可以继续监控。最后,对两个开源SN系统进行了研究,结果表明了本方法的有效性,且检测出两个系统中存在某些违反安全性质的情况。