BGV: Symbolic Noise Analysis for Dependency Tracking

[ZenithalHourlyRate]

Status

This PR is intended for the symbolic part Symbolic.h/Symbolic.cpp, as this part is big enough.

Also it should be rebased after #1816 is in.

The BGV adoption of it is not comprehensive as it only supports addition/multiplication but it is enough to demonstrate along with (#1782, which would be another PR). Its complete version supporting modulus switching/key switching needs another PR regarding SelectVariableNames. Its extension to BFV is already in a branch (also need SelectVariableNames). CKKS noise analysis could also benefit from it but lets wait until all the TODOs in #1685.

Backgrounds

Recent attacks like GNSJ24, CCP+24, CSBB24 demonstrated that the ability for noise analysis to handle dependent ciphertext is crucial for security.

These attacks exploited the fact that dependency among ciphertext will lead to faster noise growth, and former average-case analysis is not so able to handle them (strong independency assumption).

This approach could handle it but there are some issues. One obvious issue is that is could not scale-up as the number of symbolic terms grows exponentially with the number of multiplication (though there are some optimizations).

HEIR formerly has a pass called openfhe-count-add-and-key-switch in #1254 that could in spirit handle those attacks but it is standalone and not connected to the NoiseAnalysis inside HEIR.

Some experiments

Multiplication of Independent ciphertext

func.func @mul(%arg0 : i16 {secret.secret}, %arg1 : i16 {secret.secret}) -> i16 {
  %1 = arith.muli %arg0, %arg1 : i16
  return %1 : i16
}

MP24 model

Propagating 28.05 to <block argument> of type 'i16' at index: 0
Propagating 28.05 to <block argument> of type 'i16' at index: 1
Propagating 58.94 to %1 = arith.muli %input0, %input1
Propagating 58.94 to %2 = mgmt.relinearize %1
Propagating 24.08 to %3 = mgmt.modreduce %2

Symbol model: able to handle common dependency like secret key and error in public key (namely #1782)

Propagating 28.05 ... block arg
Propagating 28.05 ... block arg
Propagating 59.23 ... muli

Multiplication of same ciphertext

func.func @mul(%arg0 : i16 {secret.secret}) -> i16 {
  %1 = arith.muli %arg0, %arg0 : i16
  return %1 : i16
}

MP24: the same as above

Symbol: even higher noise

Propagating 59.73 ... muli

Addition of 4 indep ciphertext

func.func @mul(
  %arg0 : i16 {secret.secret},
  %arg1 : i16 {secret.secret},
  %arg2 : i16 {secret.secret},
  %arg3 : i16 {secret.secret}
  ) -> i16 {
  %1 = arith.addi %arg0, %arg1 : i16
  %2 = arith.addi %1, %arg2 : i16
  %3 = arith.addi %2, %arg3 : i16
  return %3 : i16
}

MP24

Propagating 28.05 to <block argument> of type 'i16' at index: 0
Propagating 28.55 to %1 = arith.addi %input0, %input1
Propagating 28.55 to %2 = arith.addi %input2, %input3 
Propagating 29.05 to %3 = arith.addi %1, %2 

Symbol (should align with MP24)

Propagating 28.05 <block argument>
Propagating 28.55 ... to %1 = arith.addi %input0, %input1 
Propagating 28.55 ... to %2 = arith.addi %input2, %input3
Propagating 29.05 ... to %3 = arith.addi %1, %2

Addition of same ciphertext 4 times

func.func @mul(%arg0 : i16 {secret.secret}) -> i16 {
  %1 = arith.addi %arg0, %arg0 : i16
  %2 = arith.addi %1, %1 : i16
  return %2 : i16
}

MP24 (unable to handle faster growth)

Propagating 28.05 to <block argument>
Propagating 28.55 to %1 = arith.addi %input0, %input0
Propagating 29.05 to %2 = arith.addi %1, %1

Symbol

Propagating 28.05 block arg
Propagating 29.05 addi
Propagating 30.05 addi

[j2kun]

I think the design of these symbolic classes could be improved somewhat.

Some issues I see:

• Storing this map on each instance of this class is quite wasteful.
• The repeated calls to updateMonomials and updateSymbols seem like they could have performance issues.

I think a more typical design for a symbolic expression system would involve separating the syntax from the semantics in the following sense:

• Symbol is an abstract opaque concept that has a kind and a name, but no param. Two symbols are compared for equality purely by their name.
• Expression is a syntactic combination of symbols according to one of multiple options. The multivariate polynomial class you made is basically there, but the design choice here would be to separate the evaluation step from the representation of the expression itself.
  • Another option (which may be simpler and more reusable, but slightly more work right now) would be to represent the symbolic expression more generically as a tree, with leaf nodes for symbols and constants, and interior nodes for add, mul, variance, etc., and then before evaluating it you could identify critical substructures like Var(s^j e^k) and collapse them into a distinguished node type.
• Interpreter (a new class) provides a mapping from symbols to concrete values, replacing the role of param as a member variable on Symbol, and has an evaluate method that can evaluate expressions and symbols recursively. An instance of Interpreter would be attached to the noise model and invoked inside toLogBound with the concrete parameters known at that time.

With this design, any combination of two symbolic expressions need only concern itself with its internal representation of the expression (i.e., grouping like terms), and the interpreter handles the implementation detail of using NoiseState to run the evaluation (or it could do something else).

In my view, there are going to be a number of places in HEIR that will want symbolic expression trees (operation rebalancer, this noise model, polynomial evaluation lowerings). I think it may be worthwhile to combine all those partial solutions into one shared library, and the design I sketched above would be close to what we do. So having this PR align closer to that ideal is what I'm after.