PaperlayerView exact revision on arXiv

Source-linked AI summary

CrypTFlow: Secure TensorFlow Inference

Nishant Kumar, Mayank Rathee, Nishanth Chandran, Divya Gupta, Aseem Rastogi, Rahul Sharma

arXiv:1909.07814v2cs.CRcs.LGcs.PL

TL;DR

Secure inference has been difficult to make both easy to use and scalable to large neural networks. CrypTFlow addresses this by compiling TensorFlow into MPC through Athos, accelerating semi-honest inference with Porthos, and deriving malicious security with Aramis; it reaches ImageNet-scale inference in about 30 seconds semi-honestly and under two minutes maliciously.

  • Problem

    Secure inference must become effortless to use while handling large ImageNet-scale deep neural networks, beyond prior work on small MNIST or CIFAR benchmarks.

  • Method

    CrypTFlow combines the Athos TensorFlow-to-MPC compiler, the improved semi-honest 3-party protocol Porthos, and the hardware-assisted malicious-security transformation Aramis.

  • Results

    CrypTFlow securely runs ImageNet-scale inference with 76.45% Top 1 and 93.23% Top 5 accuracy, taking about 30 seconds semi-honestly and about 2 minutes maliciously.

  • Takeaways & Limitations

    CrypTFlow provides an end-to-end, modular path from standard TensorFlow inference code to secure protocols supporting both semi-honest and malicious security.

Abstract

from arXiv · show

We present CrypTFlow, a first of its kind system that converts TensorFlow inference code into Secure Multi-party Computation (MPC) protocols at the push of a button. To do this, we build three components. Our first component, Athos, is an end-to-end compiler from TensorFlow to a variety of semi-honest MPC protocols. The second component, Porthos, is an improved semi-honest 3-party protocol that provides significant speedups for TensorFlow like applications. Finally, to provide malicious secure MPC protocols, our third component, Aramis, is a novel technique that uses hardware with integrity guarantees to convert any semi-honest MPC protocol into an MPC protocol that provides malicious security. The malicious security of the protocols output by Aramis relies on integrity of the hardware and semi-honest security of MPC. Moreover, our system matches the inference accuracy of plaintext TensorFlow. We experimentally demonstrate the power of our system by showing the secure inference of real-world neural networks such as ResNet50 and DenseNet121 over the ImageNet dataset with running times of about 30 seconds for semi-honest security and under two minutes for malicious security. Prior work in the area of secure inference has been limited to semi-honest security of small networks over tiny datasets such as MNIST or CIFAR. Even on MNIST/CIFAR, CrypTFlow outperforms prior work.

I. INTRODUCTION

CrypTFlow targets effortless, scalable secure inference by compiling TensorFlow into MPC protocols and supporting both semi-honest and malicious security. Its components improve usability and efficiency while enabling ImageNet-scale neural-network inference without loss of classification accuracy.

  • Motivation and system: CrypTFlow converts TensorFlow inference code into MPC protocols automatically, lowering the entry barrier for ML practitioners.Athos compiles TensorFlow to multiple secure-computation backends while preserving accuracy.
  • Components: Athos compiles TensorFlow to 2-party and 3-party secure-computation protocols while matching floating-point inference accuracy.It automatically converts floating-point computation into fixed-point computation required by efficient MPC protocols.
  • Results: CrypTFlow achieves 76.45% Top 1 and 93.23% Top 5 accuracy on secure ImageNet inference, with about 30 seconds for semi-honest and about 2 minutes for malicious security.The system evaluates networks including RESNET-200, which has 200 layers and 65 million parameters.
  • Results: Prior secure-inference implementations focused on small MNIST or CIFAR networks and weaker semi-honest adversaries, whereas CrypTFlow supports larger networks and malicious security.The toolchain and benchmarks are publicly available, and it was also evaluated on medical-imaging DNNs.
  • Components: Porthos improves semi-honest 3-party inference efficiency, reducing convolution communication by up to two orders of magnitude and nonlinear-layer communication by 25%.Its redesigned Beaver-triple computation reduces convolution communication, while eliminating one share transfer cuts ReLU and MaxPool communication in half.
  • Components: Aramis converts semi-honest MPC protocols into maliciously secure protocols using hardware code attestation and secure signing, without requiring hardware confidentiality.The technique applies to any semi-honest protocol and supports a stronger adversarial model.

C. Organization of the paper

The paper organizes CrypTFlow as an end-to-end TensorFlow-to-MPC toolchain, then explains Athos and its intermediate representations, conversion steps, and optimizations. A logistic-regression example illustrates the compilation flow from TensorFlow code through graph metadata and intermediate languages.

  • II. MOTIVATING EXAMPLE: The motivating example traces vanilla TensorFlow logistic regression through graph extraction, metadata generation, and compilation toward MPC protocols.Figures 1–3 introduce the end-to-end toolchain, TensorFlow snippet, graph definition, and tensor-dimension metadata.
  • III. ATHOS: Athos compiles TensorFlow inference code into a high-level intermediate language with explicit tensor dimensions.The frontend runs the model on a dummy input to generate metadata before translating it to HLIL.
  • III. ATHOS: Athos automatically converts floating-point TensorFlow computation into fixed-point code without compromising inference accuracy.MPC protocols generally operate over integers or fixed precision, while ML models commonly use floating-point arithmetic.
  • III. ATHOS: Athos lowers floating-point HLIL into fixed-point LLIL, a C-like language supporting integer tensors, control flow, functions, and cryptographic backend interfaces.LLIL enables different cryptographic backends to be plugged into the compiler.
  • III. ATHOS: Athos applies MPC-specific optimizations and standard dataflow analyses to its statically typed intermediate representations.The paper presents HLIL syntax and explains that explicit static dimensions support compiler analyses and optimizations.

B. Float-to-fixed

Athos automatically converts floating-point TensorFlow inference into fixed-point integer computation for MPC, balancing precision against overflow while preserving practical accuracy.

  • Motivation: Floating-point ML models are converted automatically to fixed-point arithmetic because MPC protocols operate more efficiently over integers.The conversion avoids requiring programmers to manually translate or retrain models.
  • Conversion: The scale parameter s controls precision by mapping each real r to the b-bit integer floor(r · 2^s).The represented real value is obtained by dividing the integer by 2^s.
  • Accuracy: A fixed-point example produces 140.040000021457672119140625 for the desired result 140.04, and Athos is reported not to lose accuracy in practice.The paper attributes this practical behavior to normalized machine-learning values and reports supporting results in Table VI.
  • Scale selection: Athos selects s by sweeping {0, 1, ..., b−1} and choosing the value that gives the best validation accuracy.For the example computation, the most accurate result occurs at s = 24.

C. Modular LLIL

Athos uses modular intermediate representations to connect TensorFlow inference with interchangeable MPC backends and to enable static analyses and optimizations.

  • Modular LLIL: Athos compiles floating-point HLIL into integer-valued LLIL, a C-like language supporting tensors, control flow, functions, and backend interfaces.LLIL is subsequently compiled into MPC protocol code.
  • Backend modularity: LLIL separates share-manipulating primitives implemented by cryptographic backends from ordinary functions supplied through a reusable library.Athos provides implementations using ABY, SecureNN, and Porthos backends.
  • Analysis and optimization: Static analyses over explicit LLIL tensor dimensions support optimizations such as reaching definitions, liveness analysis, and memory savings up to 80%.The explicit dimensions make analyses possible after TensorFlow’s dynamic Python typing is reconciled with static HLIL typing.
  • Analysis and optimization: A peephole pass replaces MaxPool(ReLU(·)) with the more efficient ReLU(MaxPool(·)) pattern for protocols reducing these operations to secure comparisons.The transformation reduces the number of comparisons relative to the conventional layer expression.
  • Porthos integration: Porthos reduces communication in both linear and nonlinear DNN layers by modifying convolution, ReLU, and MaxPool protocols.The approach trades communication for computation and reports convolutional gains that improve with larger filters.
  • Porthos integration: Load balancing activation work between P0 and P1 reduces the overall communication of ShareConvert, ComputeMSB, ReLU, and MaxPool by 25%.The optimization halves communication on the critical path when activations are computed in parallel.

V. ARAMIS

Aramis converts semi-honest MPC protocols into maliciously secure protocols using hardware integrity guarantees while retaining the original corruption threshold.

  • Goal: Aramis is a general technique for converting any semi-honest secure MPC protocol into one tolerating malicious corruptions.The malicious protocol retains the semi-honest protocol’s threshold of corrupted parties.
  • Trust model: Aramis relies on a minimal hardware-integrity assumption: code attestation ensures outputs come from the attested code.The threat model places the host operating system outside the trusted computing base and allows observation of secure-hardware state.
  • Mechanism: Attested hardware lets parties verify that protocol messages were computed according to the semi-honest specification and consistent with inputs and prior transcripts.Messages are signed by hardware whose code can be attested by other parties.
  • Mechanism: The attestation functionality allows a function to be committed once and returns a token for attested execution.It is parameterized by a signing key pair and supports signature verification.

B. Semi-honest security to malicious security

Aramis enforces honest execution of a semi-honest protocol by attesting and verifying signed messages, yielding malicious security in the attestation-hybrid model.

  • Modified protocol: Aramis modifies the semi-honest next-message function to track inputs, randomness, rounds, and transcripts while checking message signatures.Invalid transcripts or failed verification cause the modified function to output ⊥ or abort.
  • Attested execution: Each party commits the modified next-message function to attested hardware and verifies tokens and messages received from other parties.The protocol proceeds only when the relevant verifications succeed.
  • Security result: The modified protocol securely realizes the same MPC functionality in the attestation-hybrid model against malicious adversaries.Theorem 1 derives this result when the underlying protocol is semi-honest secure and realizes the target functionality.
  • Security result: The proof preserves the underlying semi-honest protocol’s corruption threshold when moving to malicious security.The construction’s security depends on the attested execution mechanism and the semi-honest security of the original protocol.

C. Realizing Fattest

Aramis can be implemented using hardware platforms that provide code attestation and secure signing; CrypTFlow implements it with Intel SGX. In the Fattest-hybrid, enclaves verify other parties’ attestation tokens and signed protocol outputs.

  • Hardware realization: CrypTFlow implements Aramis using Intel SGX, although the hardware functionality could also be realized with several other attestation-capable platforms.Examples include STM32H7, MediaTek MT3620, CEC1702, ARMTrustZone, and Intel SGX.
  • Hardware realization: SGX enclaves attest their code and generate signed outputs whose verification key is publicly bound to the attested enclave.The enclave creates a signing key pair, includes its verification key in the attestation token, and signs computed outputs.
  • Fattest-hybrid: The Fattest-hybrid prelude verifies every party’s enclave token and obtains the verification keys needed to check inter-enclave signatures.All parties run the same function with this verification prelude attached.

D. Implementation challenges with Intel SGX

Implementing highly interactive MPC across multiple SGX enclaves is challenging because the protocols require multiple interaction rounds and large data transfers.

  • Implementation challenges: MPC across multiple SGX enclaves must support protocols involving multiple rounds of interaction and large volumes of data.These requirements create implementation challenges distinct from simpler enclave computations.

1) Memory constraints in SGX:

CrypTFlow addresses SGX memory and communication constraints through chunking, blocking, liveness analysis, and payload tuning, enabling large-scale experiments under fixed hardware and network conditions. Its protocols scale linearly with DNN depth while achieving ImageNet-scale inference runtimes.

  • Memory constraints in SGX: 128MB is the maximum EPC size, and paging encrypted evicted pages adds detrimental overhead; CrypTFlow reduces working sets to limit it.The EPC size is fixed in BIOS, so oversized enclave workloads incur paging costs.
  • Memory constraints in SGX: ReLU and MaxPool computations are split into EPC-fitting chunks, while convolution and matrix-multiplication matrices are processed in smaller blocks.For RESNET50, ReLU and MaxPool chunk sizes are 40 MB and 10 MB, respectively.
  • Memory constraints in SGX: Liveness analysis reduces RESNET50’s memory footprint from 1100 MB to 397 MB, and combining it with chunking reduces the footprint to 297 MB.Smaller chunks increase rounds, but the reported configurations trade this overhead for eliminating paging costs.
  • Implementation challenges: Payload sizes are tuned because larger enclave-bound parameters slow marshalling, whereas smaller parameters increase cross-bridge calls.Both marshalling cost and call overhead affect highly interactive SGX applications.
  • Performance and scalability: Under a 3-party LAN setup using 3.7GHz machines, 16GB RAM, and at most 377 MBps bandwidth, ImageNet-scale inference takes about 30 seconds semi-honestly and under two minutes maliciously.The malicious protocol is about 3x slower than the semi-honest version.
  • Performance and scalability: Communication and runtime increase linearly with DNN depth across RESNET-n benchmarks from 18 to 200 approximate convolutional layers.The largest benchmark, RESNET-200, has 65 million parameters.

B. Comparison with prior work

CrypTFlow is evaluated against prior secure-inference systems on their small MNIST and CIFAR-10 benchmarks, while also comparing fixed-point accuracy, backend modularity, and Porthos against SecureNN. Across these evaluations, it reports stronger performance while preserving inference accuracy and supporting multiple MPC backends.

  • Comparison with prior secure inference: Porthos outperforms prior and concurrent semi-honest 3PC systems on MNIST, including ABY3, Chameleon, SecureNN, and QuantizedNN.The comparison uses benchmarks with similar bandwidth and compute to prior work.
  • Comparison with prior secure inference: Chameleon’s online phase is 2PC, but its offline phase requires a trusted third party; the reported comparison uses overall time.This qualification affects how its timing should be interpreted.
  • Athos experiments: Athos-generated fixed-point code matches floating-point accuracy on RESNET50 and DENSENET121, with precision selected per benchmark.Sweeping through precision levels is reported as effective for maximizing classification accuracy.
  • Athos experiments: CRYPTFLOW can compile to the semi-honest 2PC ABY backend and run both logistic regression and a small LeNet network.This demonstrates modularity across MPC backends and model types.
  • Porthos experiments: Porthos reduces communication by roughly 1.2X–1.5X and runtime by roughly 1.4X–1.5X relative to SecureNN on ImageNet-scale benchmarks.The comparison uses SecureNN as an additional CRYPTFLOW backend.

E. Aramis experiments

Aramis provides malicious security by compiling semi-honest MPC protocols with hardware integrity guarantees, while CrypTFlow demonstrates efficient secure inference on large and healthcare-focused networks.

  • Aramis: 54% was the maximum reported overhead of Aramis-based malicious security relative to the semi-honest protocol.The measurement covers functions evaluated with the GMW protocol.
  • Aramis: 10X/46X/44X/15X faster performance was achieved by Aramis on four MNIST benchmarks than QuantizedNN’s crypto-only malicious protocol.The comparison uses 3PC with one corruption for both approaches.
  • Healthcare applications: No accuracy loss was observed during secure DenseNet121 inference for chest X-ray disease prediction, with runtime similar to ImageNet DenseNet121.The underlying model reported an average AUROC of 0.845 across 14 disease labels.
  • Healthcare applications: 30 seconds was sufficient for secure diabetic-retinopathy prediction with CrypTFlow.The task predicts whether a retinal image has diabetic retinopathy.
  • Aramis: Aramis converts semi-honest MPC protocols into maliciously secure protocols using hardware integrity guarantees.Its security relies on hardware integrity and the semi-honest security of the underlying MPC protocol.
  • System scope: CrypTFlow’s modular design supports multiple MPC backends and is intended as a testbed for benchmarking new protocols.The system includes TensorFlow compilation, an improved semi-honest 3PC protocol, and conversion to malicious security.

APPENDIX

The appendix describes tensor reshaping procedures, batch-normalization handling, and ImageNet accuracy experiments comparing secure computation approaches.

  • Tensor transformations: Porthos uses ReshapeFilter, input reshaping, and ReshapeOutput procedures to prepare convolution data for its protocol.The listed algorithms transform filters and tensor layouts through nested index mappings.
  • Batch Normalization: Batch normalization uses batch mean and variance, learned parameters γ and β, and inference statistics from the entire training dataset.The appendix defines the normalization operation for an input x and states that inference uses training-dataset statistics.
  • Performance comparison: 3PC protocols like Porthos are reported as much faster than 2PC/FHE-based approaches in the appendix comparison.The comparison appears in Table X, whose times are reported in seconds.

E. Proof of malicious security

The malicious-security proof argues that hardware-backed verification forces corrupted parties to follow the semi-honest protocol or causes honest parties to abort, yielding standard MPC security.

  • Security intuition: Aramis constrains a malicious party to execute the semi-honest protocol faithfully, with deviations causing an honest party to abort.The argument is presented for a single malicious party and extended to colluding corrupt parties.
  • Message integrity: Signature unforgeability prevents corrupted parties from forging incorrectly generated protocol messages under honest or corrupted parties’ verification keys.The hardware-backed functions also provide correct randomness for generating semi-honest protocol messages.
  • Security theorem: Protocol Protmalicious securely realizes the MPC functionality in the attest-hybrid model against malicious adversaries.Theorem 2 assumes that the underlying protocol securely realizes the target functionality against semi-honest adversaries.
  • Simulation proof: The simulator uses the semi-honest simulator and verifies corrupted-party tokens, inputs, function descriptions, and protocol messages.Verification failures cause an abort, while accepted inputs are submitted to the ideal MPC functionality.
  • Proof conclusion: The proof concludes security through the standard simulation paradigm for the protocol shown in Figure 8.The real and ideal executions are argued indistinguishable using semi-honest security of the underlying protocol.
Loading 1909.07814v2…