01715nas a2200181 4500008004100000245004900041210004900090260001400139300001200153490000600165520119200171653003801363653004301401100001401444700001901458700001901477856003701496 2023 eng d00aFat Pointers for Temporal Memory Safety of C0 aFat Pointers for Temporal Memory Safety of C c3/20/2023 a316-3470 v73 a

Temporal memory safety bugs, especially use-after-free and double free bugs, pose a major security threat to C programs. Real-world exploits utilizing these bugs enable attackers to read and write arbitrary memory locations, causing disastrous violations of confidentiality, integrity, and availability. Many previous solutions retrofit temporal memory safety to C, but they all either incur high performance overhead and/or miss detecting certain types of temporal memory safety bugs.
In this paper, we propose a temporal memory safety solution that is both efficient and comprehensive. Specifically, we extend Checked C, a spatially-safe extension to C, with temporally-safe pointers. These are implemented by combining two techniques: fat pointers and dynamic key-lock checks. We show that the fat-pointer solution significantly improves running time and memory overhead compared to the disjoint-metadata approach that provides the same level of protection. With empirical program data and hands-on experience porting real-world applications, we also show that our solution is practical in terms of backward compatibility -- one of the major complaints about fat pointers.

10aCryptography and Security (cs.CR)10aFOS: Computer and information sciences1 aZhou, Jie1 aCriswell, John1 aHicks, Michael uhttps://arxiv.org/abs/2208.1290001906nas a2200205 4500008004100000245008600041210006900127260001400196520121200210653004301422653002701465653003801492653003401530653003101564100001901595700001301614700001701627700001901644856003701663 2022 eng d00aQunity: A Unified Language for Quantum and Classical Computing (Extended Version)0 aQunity A Unified Language for Quantum and Classical Computing Ex c4/26/20223 a

We introduce Qunity, a new quantum programming language designed to treat quantum computing as a natural generalization of classical computing. Qunity presents a unified syntax where familiar programming constructs can have both quantum and classical effects. For example, one can use sum types to implement the direct sum of linear operators, exception-handling syntax to implement projective measurements, and aliasing to induce entanglement. Further, Qunity takes advantage of the overlooked BQP subroutine theorem, allowing one to construct reversible subroutines from irreversible quantum algorithms through the uncomputation of "garbage" outputs. Unlike existing languages that enable quantum aspects with separate add-ons (like a classical language with quantum gates bolted on), Qunity provides a unified syntax and a novel denotational semantics that guarantees that programs are quantum mechanically valid. We present Qunity's syntax, type system, and denotational semantics, showing how it can cleanly express several quantum algorithms. We also detail how Qunity can be compiled into a low-level qubit circuit language like OpenQASM, proving the realizability of our design.

10aFOS: Computer and information sciences10aFOS: Physical sciences10aLogic in Computer Science (cs.LO)10aProgramming Languages (cs.PL)10aQuantum Physics (quant-ph)1 aVoichick, Finn1 aLi, Liyi1 aRand, Robert1 aHicks, Michael uhttps://arxiv.org/abs/2204.1238401360nas a2200229 4500008004100000020002200041022001400063245003700077210003700114260001200151300001700163490000800180520076100188100001900949700001700968700001900985700001301004700001901017700001701036700002101053856005601074 2021 eng d a978-3-95977-188-7 a1868-896900aProving Quantum Programs Correct0 aProving Quantum Programs Correct c06/2021 a21:1–21:190 v1933 a

As quantum computing progresses steadily from theory into practice, programmers will face
a common problem: How can they be sure that their code does what they intend it to do? This
paper presents encouraging results in the application of mechanized proof to the domain of quantum
programming in the context of the sqir development. It verifies the correctness of a range of a
quantum algorithms including Grover’s algorithm and quantum phase estimation, a key component
of Shor’s algorithm. In doing so, it aims to highlight both the successes and challenges of formal
verification in the quantum context and motivate the theorem proving community to target quantum
computing as an application domain.

1 aHietala, Kesha1 aRand, Robert1 aHung, Shih-Han1 aLi, Liyi1 aHicks, Michael1 aCohen, Liron1 aKaliszyk, Cezary uhttps://drops.dagstuhl.de/opus/volltexte/2021/13916