Ongoing work:

Verifying the safety of a MPC/SMCprotocol & language by Coq
Greg Weng TPP 2023

Greg Weng
2023.Feb: Mercari R4D program -> Nagoya University Ph.D. student (大学院多元数理科学研究科)
2019 ~: Mercari, software engineer: Golang
2017 - 2019: Rakuten, software engineer: JavaScript2014 - 2017: Mozilla Taipei, software engineer: C, C++, JavaScript
2012 - 2014: National Chengchi University (Taiwan), CS department (master's degree): Haskell, Ruby

Research BackgroundAs a building block ofMPC/SMC

SMC Scalar-productProtocol

Secure Multi-party Computation
As a building block of

Is Based on

Commodity Server Model

SMC Protocols
As building blocks ofsmcSL
DSL for MPC/SMC

Research BackgroundAs a building block of

MPC/SMCSMC Scalar-productProtocol

Secure Multi-party Computation

By pen-and-paper has been proven

As a building block of

Is Based on

SMC Protocols

Commodity Server Model

As building blocks ofsmcSL
DSL for MPC/SMC
May have issues of

Implicit Information Flow
Leakage from a safe protocol & language

Information Theoretic Safe

Research BackgroundAs a building block of

MPC/SMCSMC Scalar-productProtocol

Secure Multi-party ComputationBy pen-and-paper has been proven

As a building block of

Is Based on

SMC Protocols

Commodity Server Model

Information Theoretic Safe

As building blocks ofsmcSL

Can be used inCoq

DSL for MPC/SMC

Zero-Knowledge Protocol

May have issues of

Implicit Information Flow
Leakage from a safe protocol & language

Quantitative Analysis ofInformation Flow

Research BackgroundAs a building block of

MPC/SMCSMC Scalar-productProtocol

Secure Multi-party Computation

By pen-and-paper has been proven

As a building block of

Is Based on

Can be used in?

Commodity Server Model

SMC Protocols

Information Theoretic Safe

As building blocks ofsmcSL

Can be used inProofs in ?

CoqDSL for MPC/SMC

Zero-Knowledge Protocol

Analyzed by ?

May have issues of

Implicit Information Flow
Leakage from a safe protocol & language

Quantitative Analysis ofInformation Flow

MPC/SMC
MPC/SMC stands for "Multi-Party Computation"and "Secure Multi-party Computation"
It is a security domain about two or more parties
collaboratively compute results, without revealingeach party's secret data over what they agree toshare.
Nowadays this tech is also used for digital wallet

Neither A nor B agree to reveal their bidding price
Both of them want to know the bidding result (A >? B)--> This indirectly reveal other properties of their secrets:
If not (A > B),
for A, a new fact is that B's price is larger than $500
for B, a new fact is that A's price is smaller than $900

Commodity Server Model MPC/SMC
It is a model proposed by Wenliang Du andZhijun Zhan*, to simplify the infrastructure
and computation difﬁculties for two and moreparties, by introducing a "commodity server"in the MPC/SMC computation ﬂow.
The only role of this commodity server, is toissue necessary random values to guarantee
when Alice and Bob compute collaboratively
With MPC/SMC protocols, no one should
obtain more information than they agree toshare, from the data they pass to each other.

Commodity
Serverrandom values

Alice

Bob

Two-Party Model

Alicerandom values

Bob

Commodity-Server Model* Wenliang Du, Zhijun Zhan. A practical approach to solve Secure Multi-party Computation problems. NSPW 2002: Proceedings of the 2002 Workshop on New Security Paradigms; 2002 Sep 23-26;
Virginia Beach, Virginia USA. New York, NY, USA: ACM Press; 2002. p. 127-35.

Scalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref1
For example:Xa = (3), Xb = (2)Commodity Ra, Rb, ra, rb = (9), (8), 13, 59
Results ya, yb = -60, 66
ya + yb = 6 = (3) . (2) = Xa . Xb
Local inputs: Xa, Xb
Shared output: ya, yb→ Alice and Bob collaboratively computed the result y = ya + yb, where y = Xa . Xb
→ If numbers are real numbers*, Alice and Bob cannot know each other's secret vectors

Scalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref1
Commodity
ServerCommodity
ServerRa, ra(9), 13

Commodity
Server
Rb, rb = Ra.Rb - ra(8),= 59

Alice

Bob

Alice

Bob

Xa = (3)

Xb = (2)Xa = (3)

Xb = (2)Ra, ra(9), 13
Alice
Xa = (3)Xa' = (12) = Xa + Ra

Rb, rb(8), 59
Bob
Xb = (2)Xb' = (10) = Xb + Rb

Generate then send to each otherScalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref1
Commodity
ServerRa, ra(9), 13

Commodity
ServerRb, rb(8), 59

Ra, ra(9), 13

Alice

Bob

Alice

Xa = (3)
Xb' = (10)Xb = (2)Xa' = (12)Xa = (3)
Xb' = (10)Commodity
ServerRb, rb(8), 59
Bob

Xb = (2)Xa' = (12)yb = 66 from RNG
t = (Xb . Xa') + rb - yb
= 24 + 59 - 66
= 17

Generate then send toRa, ra(9), 13
Alice
Xa = (3)
Xb' = (10)t= 17

Rb, rb(8), 59
Bob
Xb = (2)Xa' = (12)yb = 66 from RNG

Scalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref1
CommodityServerCommodity
ServerRa, ra(9), 13
Alice
Xa = (3)
Xb' = (10)t= 17ya = t - (Ra . X'b) + ra
= 17 - 90 + 13
= -60

Rb, rb(8), 59

Ra, ra(9), 13
Alice

Bob
Xb = (2)Xa' = (12)yb = 66 from RNG

Rb, rb(8), 59Xa
ya= (3)
= -60

Bob
Xb
yb= (2)= 66y = 6 = ya + yb = Xa . Xb

Scalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref1
(Alice, Bob) holdLocal inputs (Xa, Xb)
Shared outputs (ya, yb)
This Scalar-product protocol can be denoted as ref2:Scalar-product based MPC/SMC protocols[Scalar product protocol -- Commodity server approach] ref2

By this basic building block, Academia Sinica in Taiwan built other secure protocols for MPC/SMC arithmetic
operations, including comparison, conditional expression, etcref2 .
In following research ref3, more protocols were invented to support both integers and ﬂoating points.

Scalar-product based MPC/SMC protocolsref2[Scalar product protocol -- y = Xa . Xb]

Scalar-product based MPC/SMC protocolsref2[Conditional expression -- Alice ba xa ya, Bob bb xb yb,result: (b ? xa + xb : ya + yb)]

Commodity
ServerAlice

Bob

Local Inputs:(ba, xa, ya)(bb, xb, yb)

Protocol Outputs:

zazbz =Scalar-product based MPC/SMC protocolsref2[Product -- Alice: xa ya, Bob: xb yb, result: z = x* y]

Commodity
ServerAlice

Bob

Local Inputs:(xa, ya)(xb, yb)

Protocol Outputs:zazbz = za + zb = (xa + xb) * (ya + yb) = x * yAll protocols are from: Shen, Chih-Hao, Justin, Zhan, Tsan-Sheng, Hsu, Churn-Jung, Liau, and Da-Wei, Wang. "Scalar-product based
secure two-party computation." . In 2008 IEEE International Conference on Granular Computing (pp. 556-561).2008.

Scalar-product, protocols, and the scripting language
Compose SMC program in smcSL
To invoke SMC protocols safely[Comparison][Z2-to-Zn][Division][Zn-to-Z2][ConditionalExpression][Product]

From Weng, Cheng-Hui, Chen Kung, "A Modular Scripting
Language for Secure Multi-Party Computation", master thesis[Scalar product protocol -- y = Xa . Xb,(commodity approach)] Ref.1[Scalar product protocol -- y = Xa . Xb,(commodity approach)]

Arrow means: A -(is used to build)->B

SMC Scalar-productis used to build

SMC Protocols

Ref.2

is used to build

SMC Scripting Language (smcSL)

Application: Public health data analysisref8
Chen, K., Hsu, T. S., Huang, W. K., Liau, C. J., &Wang, D. W. (2012). Towards a Scripting
Language for Automating Secure Multiparty
Computation.

CommodityServerCDC

NHI

CDC Local Inputs: Array of (0,1,0,0,.....1) (length: 23 millions; population in Taiwan )Meaning: #N person got Dengue fever (a seasonal epidemic) = 1 or 0
NHI Local Inputs: Array of (0,1,0,0,.....1) (length: 23 millions; population in Taiwan )Meaning: #N person in the past season receive outpatient or hospitality services due to Dengue fever
Result: Array of (1,0,0,0,.....0) (length: 23 millions)
Meaning: how much did the Dengue fever cost in this seasonSMC Protocols used: conditional expression:
total := CDC[i] == NHI[i] ? total+1 : total

Research Goal: Veriﬁcation in Coq (SMC protocols)

1.

Verify SMC Scalar-product (require: list/vector libs) (GitHub repo: weng-chenghui/smc-coq)

2.

Build protocols as ref.2 describes and prove their properties

3.

Export them as module functions

4.

Make protocols in the form (Xa, Xb)-> (ya, yb) Monadica.

`->` may be a SMC interface operation for different instancesb.

Find some laws like in the paper Just do it: simple monadic equational reasoning Ref5

Research Goal: Veriﬁcation in Coq (smcSL)

Three types of monad: Local, Observation, Command (reference: monae)
1.

Local: where actual states are manipulated

2.

Observation: where traces for reasoning can be collected -- inputs and outputs
to each local

3.

Command: where smcSL program interpreted to SMC protocol executations

4.

Formalize the information ﬂow like in the paper:
Quantitative information ﬂow with monads in haskell Ref6

The original motivation: even if protocols have been provensafe ref3 , the information ﬂow may still leak somethinghas been proven information-theoretically saferef3

can still leak some information if it builds theconditional loop as a language feature→ implicit information ﬂow→ how to detect and how to quantify the leakage?

Just do it: simple monadic equational reasoningRef5
Authors: Jeremy Gibbons and Ralf Hinze
It shows:
1.

How to prove a program's claims by reasoning each monadic program step

2.

These reasoning steps (and thus the proof) are instance-independanta.

With only the monadic interface, one can claim and prove properties without knowing the instance→ SMC protocols can be described in monadic steps, and thus their claims can be reasoned in the same way→ Especially these protocols are actually used by the domain-speciﬁc language: smcSL

Quantitative information ﬂow with monads in haskellRef6
Authors: Jeremy Gibbons, Annabelle McIver, Carroll Morgan, Tom Schrijvers
It shows:
1.

How to deﬁne a Monad with probability and combine it with the information leakage analysisa.

2.

Tracing how much information will be leaked in programs that are composed by leaking monadic operations

A language (Kuifje) and use it to analyze information leakage with state updating programs→ A related work for analyzing smcSL→ Yet the issue "protocols are safe but progam leaks information" still need some more work

Possible extensions
1.

Extend the commodity-server-based SMC scalar product to N parties, not just two partiesa.

Instead of scalar product, determinant seems to have the potential to extend the protocol to N partiesb.

But need to solve the problem of padding numbers when inputs cannot form a square matrix

2.

And also extend the SMC protocols build on it

3.

With Coq veriﬁcation

4.

Use and extend this N parties SMC protocol to the zero-knowledge-protocol that described in the paper ref7:
Zero-knowledge from secure multiparty computation

Zero-knowledge from secure multiparty computationref7
Authors: Yuval Ishai, Eyal Kushilevitz, Rafail Ostrovsky, Amit Sahai
It shows:
1.

A N-party MPC/SMC program can be used as a problem in ZKP with lower cost compared to 3-coloring
problem or Hamiltonicity

2.

The zero-knowledge protocol use such a MPC/SMC program can satisfy three properties (completness,soundness, and zero-knowledge), even if there are some corrupted MPC/SMC players

Diﬃculties & ﬁnds
1.

Coq

2.

Work & Study at the same time3.

Culture shock: academic vs. industrial documents, codes, discussions, and strategies to solve problems

Diﬃculties & ﬁnds (Coq)As a software engineer, most of time people expect to ﬁnd immediately usable examples or specs.
Or at least with only code, it is still readable to understand how the code work.
Also with API references, one should be able to complete most of work without asking anyone.

Diﬃculties & ﬁnds (Coq)As a Ph.D. student,

Most of time people expect to ﬁnd immediately usable examples or specs.
Or at least with only code, it is still readable to understand how the code work.
Also with API references, one should be able to complete most of work without asking anyone.

→ I'm still trying to get used to Coq coding style (with SSReﬂect) ,and how to accept myself when a single // blocks me to parse the whole proof,
or when there is a bug in old Coq code, by adding some magic terms or splitting steps the issues are gone

Diﬃculties & ﬁnds (culture shock)
As a software engineer, most of time we are asked to workaround issues & copy existing solutions to meet business
requirements.
There is no time and no priority to study and solve a problem thoroughly, or create something with comprehensive design.

For solving problems

For building something new1.

Can we reduce the impact to end
users, or other systems?

1.

Can we reach business requirements fast andcheap?

2.

Can we solve it within one week?

2.

3.

Is there any existing workaround orsolution we can easily apply?

If generalization means no one can see its value,
we choose copying code and specializing it for one
business purpose.

4.

Does this problem with reduced
impact, really worth to solve?

3.

"Edge cases" = never need to prevent them fromhappening, unless they really happen

Diﬃculties & ﬁnds (culture shock)Also as a software engineer, people expect to output some results within reasonable time
Or if after a while we cannot have the expected result, at least we know the reason

Diﬃculties & ﬁnds (culture shock)Also as a software engineer, people expect to output some results within reasonable time.
Or if after a while we cannot have the expected result, at least we know the reason.
And how much resource we already spent, and if we continue, how much we will spend.

Result <-> Time <-> People <-> Priority <-> Impact

Diﬃculties & ﬁnds (culture shock)Also as a software engineer, people expect to output some results within reasonable time.
Or if after a while we cannot have the expected result, at least we know the reason.
And how much resource we already spent, and if we continue, how much we will spend.

Result <-> Time <-> People <-> Priority <-> Impact
As a Ph.D. student, there are so many possible paths, papers, ideas, things-to-study that may all lead to a dead end.

Result <?> Time <?> People <?> Priority <?> Impact

Q&A

References
1.

Wenliang Du, Zhijun Zhan. A practical approach to solve Secure Multi-party Computation problems. NSPW 2002: Proceedings of the 2002
Workshop on New Security Paradigms; 2002 Sep 23-26; Virginia Beach, Virginia USA. New York, NY, USA: ACM Press; 2002. p. 127-35.

2.

Shen, Chih-Hao, Justin, Zhan, Tsan-Sheng, Hsu, Churn-Jung, Liau, and Da-Wei, Wang. "Scalar-product based secure two-party computation." In2008 IEEE International Conference on Granular Computing (pp. 556-561).2008.

3.

Wang, D. W., Liau, C. J., Chiang, Y. T., & Hsu, T. S. (2006). Information theoretical analysis of two-party secret computation. In Data and Applications
Security XX: 20th Annual IFIP WG 11.3 Working Conference on Data and Applications Security, Sophia Antipolis, France, July 31-August 2, 2006.
Proceedings 20 (pp. 310-317). Springer Berlin Heidelberg.

4.

Weng, Cheng-Hui, Chen Kung "模組化之安全多方計算領域專屬腳本語言 A Modular Scripting Language for Secure Multi-Party Computation"

5.

Gibbons, J., & Hinze, R. (2011). Just do it: simple monadic equational reasoning. ACM SIGPLAN Notices, 46(9), 2-14.

6.

Gibbons, J., McIver, A., Morgan, C., & Schrijvers, T. (2019). Quantitative information ﬂow with monads in haskell. Foundations of ProbabilisticProgramming.

7.

Ishai, Y., Kushilevitz, E., Ostrovsky, R., & Sahai, A. (2007, June). Zero-knowledge from secure multiparty computation. In Proceedings of thethirty-ninth annual ACM symposium on Theory of computing (pp. 21-30).

8.

Chen, K., Hsu, T. S., Huang, W. K., Liau, C. J., & Wang, D. W. (2012). Towards a Scripting Language for Automating Secure Multiparty Computation.