More Like this

1. Verified sequential Malloc/Free

   https://doi.org/10.1145/3381898.3397211  

   Appel, Andrew W.; Naumann, David A. (June 2020, International Symposium on Memory Management)

   null (Ed.)

   We verify the functional correctness of an array-of-bins (segregated free-lists) single-thread malloc/free system with respect to a correctness specification written in separation logic. The memory allocator is written in standard C code compatible with the standard API; the specification is in the Verifiable C program logic, and the proof is done in the Verified Software Toolchain within the Coq proof assistant. Our "resource-aware" specification can guarantee when malloc will successfully return a block, unlike the standard Posix specification that allows malloc to return NULL whenever it wants to. We also prove subsumption (refinement): the resource-aware specification implies a resource-oblivious spec. 

   more » « less
2. Carrollian Amplitudes from Strings

   https://doi.org/10.1007/JHEP04(2024)127  

   Stieberger, Stephan; Taylor, Tomasz R; Zhu, Bin (April 2024, Journal of High Energy Physics)

   Carrollian holography is supposed to describe gravity in four-dimensional asymptotically flat space-time by the three-dimensional Carrollian CFT living at null infinity. We transform superstring scattering amplitudes into the correlation functions of primary fields of Carrollian CFT depending on the three-dimensional coordinates of the celestial sphere and a retarded time coordinate. The power series in the inverse string tension is converted to a whole tower of both UV and IR finite descendants of the underlying field-theoretical Carrollian amplitude. We focus on four-point amplitudes involving gauge bosons and gravitons in type I open superstring theory and in closed heterotic superstring theory at the tree-level. We also discuss the limit of infinite retarded time coordinates, where the string world-sheet becomes celestial. 

   more » « less
3. $$ \mathcal{N} $$ = 4 Super-Yang-Mills correlators at strong coupling from string theory and localization

   https://doi.org/10.1007/JHEP12(2019)119  

   Binder, Damon J.; Chester, Shai M.; Pufu, Silviu S.; Wang, Yifan (December 2019, Journal of High Energy Physics)

   A bstract We compute 1 /λ corrections to the four-point functions of half-BPS operators in SU( N ) $$ \mathcal{N} $$ N = 4 super-Yang-Mills theory at large N and large ’t Hooft coupling λ = $$ {g}_{\mathrm{YM}}^2N $$ g YM 2 N using two methods. Firstly, we relate integrals of these correlators to derivatives of the mass deformed S 4 free energy, which was computed at leading order in large N and to all orders in 1 /λ using supersymmetric localization. Secondly, we use AdS/CFT to relate these 1 /λ corrections to higher derivative corrections to supergravity for scattering amplitudes of Kaluza-Klein scalars in IIB string theory on AdS 5 × S 5 , which in the flat space limit are known from worldsheet calculations. These two methods match at the order corresponding to the tree level R 4 interaction in string theory, which provides a precise check of AdS/CFT beyond supergravity, and allow us to derive the holographic correlators to tree level D 4 R 4 order. Combined with constraints from [1], our results can be used to derive CFT data to one-loop D 4 R 4 order. Finally, we use AdS/CFT to fix these correlators in the limit where N is taken to be large while g YM is kept fixed. In this limit, we present a conjecture for the small mass limit of the S 4 partition function that includes all instanton corrections and is written in terms of the same Eisenstein series that appear in the study of string theory scattering amplitudes. 

   more » « less
4. Private Analytics via Streaming, Sketching, and Silently Verifiable Proofs

   Rathee, Mayank; Zhang, Yuwen; Corrigan-Gibbs, Henry; Popa, Raluca Ada (May 2024, IEEE Security and Privacy 2024)

   We present Whisper, a system for privacy-preserving collection of aggregate statistics. Like prior systems, a Whisper deployment consists of a small set of non-colluding servers; these servers compute aggregate statistics over data from a large number of users without learning the data of any individual user. Whisper's main contribution is that its server-to-server communication cost and its server-side storage costs scale sublinearly with the total number of users. In particular, prior systems required the servers to exchange a few bits of information to verify the well-formedness of each client submission. In contrast, Whisper uses silently verifiable proofs, a new type of proof system on secret-shared data that allows the servers to verify an arbitrarily large batch of proofs by exchanging a single 128-bit string. This improvement comes with increased client-to-server communication, which, in cloud computing, is typically cheaper (or even free) than the cost of egress for server-to-server communication. To reduce server storage, Whisper approximates certain statistics using small-space sketching data structures. Applying randomized sketches in an environment with adversarial clients requires a careful and novel security analysis. In a deployment with two servers and 100,000 clients of which 1% are malicious, Whisper can improve server-to-server communication for vector sum by three orders of magnitude while each client's communication increases by only 10%. 

   more » « less
5. The ZZ annulus one-point function in non-critical string theory: A string field theory analysis

   https://doi.org/10.1007/JHEP12(2022)151  

   Eniceicu, Dan Stefan; Mahajan, Raghu; Maity, Pronobesh; Murdia, Chitraang; Sen, Ashoke (December 2022, Journal of High Energy Physics)

   A<sc>bstract</sc> We compute the ZZ annulus one-point function of the cosmological constant operator in non-critical string theory, regulating divergences from the boundaries of moduli space using string field theory. We identify a subtle issue in a previous analysis of these divergences, which was done in the context of thec= 1 string theory, and where it had led to a mismatch with the prediction from the dual matrix quantum mechanics. After fixing this issue, we find a precise match to the expected answer in both thec< 1 andc= 1 cases. We also compute the disk two-point function, which is a quantity of the same order, and show that it too matches with the general prediction. 

   more » « less