Although Secure Multiparty Computation (SMC) has seen considerable development in recent years, its use is challenging, resulting in complex code which obscures whether the security properties or correctness guarantees hold in practice. For this reason, several works have investigated the use of formal methods to provide guarantees for SMC systems. However, these approaches have been applied mostly to domain specific languages (DSL), neglecting general-purpose approaches. In this paper, we consider a formal model for an SMC system for annotated C programs. We choose C due to its popularity in the cryptographic community and being the only general-purpose language for which SMC compilers exist. Our formalization supports all key features of C -- including private-conditioned branching statements, mutable arrays (including out of bound array access), pointers to private data, etc. We use this formalization to characterize correctness and security properties of annotated C, with the latter being a form of non-interference on execution traces. We realize our formalism as an implementation in the PICCO SMC compiler and provide evaluation results on SMC programs written in C.

翻译：尽管安全多方计算（SMC）近年来取得了长足发展，但其使用仍面临挑战，导致复杂代码难以在实践中确保证安全属性或正确性保证。为此，多项研究探索了利用形式化方法为SMC系统提供保证。然而，这些方法主要应用于领域特定语言（DSL），忽视了通用编程语言。本文针对带注释的C语言程序，提出了一个SMC系统的形式化模型。我们选择C语言是因为其在密码学社区中的广泛使用，且是唯一存在SMC编译器的通用编程语言。我们的形式化支持C语言的所有关键特性——包括私有条件分支语句、可变数组（含越界访问）、私有数据指针等。利用该形式化，我们刻画了带注释C语言的正确性与安全性属性，后者表现为执行轨迹上的非干扰特性。我们在PICCO SMC编译器中实现了该形式化模型，并提供了针对C语言编写的SMC程序的评估结果。