Dependently typed programming languages allow the type system to express arbitrary propositions of intuitionistic logic, thanks to the Curry-Howard isomorphism. Taking full advantage of this type system requires defining more types than usual, in order to encode logical correctness criteria into the definitions of datatypes. While an abundance of specialized types helps ensure correctness, it comes at the cost of needing to redefine common functions for each specialized type. This dissertation makes an effort to attack the problem of code reuse in dependently typed languages. Our solution is to write generic functions, which can be applied to any datatype. Such a generic function can be applied to datatypes that are defined at the time the generic function was written, but they can also be applied to any datatype that is defined in the future. Our solution builds upon previous work on generic programming within dependently typed programming. Type theory supports generic programming using a construction known as a universe. A universe can be considered the model of a programming language, such that writing functions over it models writing generic programs in the programming language. Historically, there has been a trade-off between the expressive power of the modeled programming language, and the kinds of generic functions that can be written in it. Our dissertation shows that no such trade-off is necessary, and that we can write future-proof generic functions in a model of a dependently typed programming language with a rich collection of types.

In this thesis, we first study what is the average redundancy resulting from the universal compression of a single finite-length sequence from an unknown source. In the universal compression of a source with d unknown parameters, Rissanen demonstrated that the expected redundancy for regular codes is asymptotically d/2 log n + o(log n) for almost all sources, where n is the sequence length. Clarke and Barron also derived the asymptotic average minimax redundancy for memoryless sources. The average minimax redundancy is concerned with the redundancy of the worst parameter vector for the best code. Thus, it does not provide much information about the effect of the different source parameter values. Our treatment in this thesis is probabilistic. In particular, we derive a lower bound on the probability measure of the event that a sequence of length n from an FSMX source chosen using Jeffreys' prior is compressed with a redundancy larger than a certain fraction of d/2 log n. Further, our results show that the average minimax redundancy provides good estimate for the average redundancy of most sources for large enough n and d. On the other hand, when the source parameter d is small the average minimax redundancy overestimates the average redundancy for small to moderate length sequences. Additionally, we precisely characterize the average minimax redundancy of universal coding when the coding scheme is restricted to be from the family of two--stage codes, where we show that the two--stage assumption incurs a negligible redundancy for small and moderate length n unless the number of source parameters is small. %We show that redundancy is significant in the compression of small sequences. Our results, collectively, help to characterize the non-negligible redundancy resulting from the compression of small and moderate length sequences. Next, we apply these results to the compression of a small to moderate length sequence provided that the context present in a sequence of length M from the same source is memorized. We quantify the achievable performance improvement in the universal compression of the small to moderate length sequence using context memorization.

Thesis (Ph. D.)--University of Hawaii at Manoa, 1994. / Includes bibliographical references (leaves 159-166). / Microfiche. / xiv, 166 leaves, bound ill. 29 cm

Thesis (M.S.)--University of Delaware, 2007. / Principal faculty advisor: Guang R. Gao, Dept. of Electrical and Computer Engineering. Includes bibliographical references.

Thesis (Ph. D.)--Oregon State University, 2010. / Printout. Includes bibliographical references (leaves 88-93). Also available on the World Wide Web.

In this thesis, we try to bridge the gap between which program transformations are possible at source-level and which are possible at binary-level. While binaries are typically seen as opaque artifacts, our binary recompiler Egalito (ASPLOS 2020) enables users to parse and modify stripped binaries on existing systems. Our technique of binary recompilation is not robust to errors in disassembly, but with an accurate analysis, provides near-zero transformation overhead. We wrote several demonstration security tools with Egalito, including code randomization, control-flow integrity, retpoline insertion, and a fuzzing backend. We also wrote Nibbler (ACSAC 2019, DTRAP 2020), which detects unused code and removes it. Many of these features, including Nibbler, can be combined with other defenses resulting in multiplicatively stronger or more effective hardening. Enabled by our recompiler, an overriding theme of this thesis is our focus on deployable software transformation. Egalito has been tested by collaborators across tens of thousands of Debian programs and libraries. We coined this term egalitarian in the context of binary security. Simply put, an egalitarian analysis or security mechanism is one that can operate on itself (and is usually more deployable as a result). As one demonstration of this idea, we created a strong, deployable defense against code reuse attacks. Shuffler (OSDI 2016) randomizes function addresses, moving functions periodically every few milliseconds. This makes an attacker's job extremely difficult, especially if they are located across a network (which necessitates ping time) -- JIT-ROP attacks take 2.3 to 378 seconds to complete. Shuffler is egalitarian and defends its own code and target code simultaneously; Shuffler actually shuffles itself. We hope our deployable, egalitarian binary defenses will allow others to improve upon state-of-the-art and paint binaries as far more malleable than they have been in the past.

The way software developers edit code day-to-day tends to be repetitive, often using existing code elements. Many researchers have tried to automate the repetitive code editing process by mining specific change templates. However, such templates are often manually implemented for automated applications. Consequently, such template-based automated code editing is very tedious to implement. In addition, template-based code editing is often narrowly-scoped and low noise tolerant. Machine Learning, specially deep learning-based techniques, could help us solve these problems because of their generalization and noise tolerance capacities. The advancement of deep neural networks and the availability of vast open-source evolutionary data opens up the possibility of automatically learning those templates from the wild and applying those in the appropriate context. However, deep neural network-based modeling for code changes, and code, in general, introduces some specific problems that need specific attention from the research community. For instance, source code exhibit strictly defined syntax and semantics inherited from the properties of Programming Language (PL). In addition, source code vocabulary (possible number of tokens) can be arbitrarily large. This dissertation formulates the problem of automated code editing as a multi-modal translation problem, where, given a piece of code, the context, and some guidance, the objective is to generate edited code. In particular, we divide the problem into two sub-problems — source code understanding and generation. We empirically show that the deep neural networks (models in general) for these problems should be aware of the PL-properties (i.e., syntax, semantics). This dissertation investigates two primary directions of endowing the models with knowledge about PL-properties — (i) explicit encoding: where we design models catering to a specific property, and (ii) implicit encoding: where we train a very-large model to learn these properties from very large corpus of source code in unsupervised ways. With implicit encoding, we custom design the model to cater to the need for that property. As an example of such models, we developed CODIT — a tree-based neural model for syntactic correctness. We design CODIT based on the Context Free Grammar of the programming language. Instead of generating source code, CODIT first generates the tree structure by sampling the production rule from the CFG. Such a mechanism prohibits infeasible production rule selection. In the later stage, CODIT generates the edited code conditioned on the tree generated earlier. Suchconditioning makes the edited code syntactically correct. CODIT showed promise in learning code edit patterns in the wild and effectiveness in automatic program repair. In another empirical study, we showed that a graph-based model is better suitable for source code understanding tasks such as vulnerability detection. On the other hand, with implicit encoding, we use a very large (with several hundred million parameters) yet generic model. However, we pre-train these models on a super-large (usually hundreds of gigabytes) collection of source code and code metadata. We empirically show that if sufficiently pre-trained, such models are capable enough to learn PL properties such as syntax and semantics. In this dissertation, we developed two such pre-trained models, with two different learning objectives. First, we developed PLBART— the first-ever pre-trained encoder-decoder-based model for source code and show that such pre-train enables the model to generate syntactically and semantically correct code. Further, we show an in-depth empirical study on using PLBART in automated code editing. Finally, we develop another pre-trained model — NatGen to encode the natural coding convention followed by developers into the model. To design NatGen, we first deliberately modify the code from the developers’ written version preserving the original semantics. We call such transformations ‘de-naturalizing’ transformations. Following the previous studies on induced unnaturalness in code, we defined several such ‘de-naturalizing’ transformations and applied those to developer-written code. We pre-train NatGen to reverse the effect of these transformations. That way, NatGen learns to generate code similar to the developers’ written by undoing any unnaturalness induced by our forceful ‘de-naturalizing‘ transformations. NatGen has performed well in code editing and other source code generation tasks. The models and empirical studies we performed while writing this dissertation go beyond the scope of automated code editing and are applicable to other software engineering automation problems such as Code translation, Code summarization, Code generation, Vulnerability detection,Clone detection, etc. Thus, we believe this dissertation will influence and contribute to the advancement of AI4SE and PLP.

Wireless multimedia sensor networks (WMSNs) are networks of interconnected devices that allow retrieving video and audio streams, still images, and scalar data from the environment. In a densely deployed WMSN, there exists correlation among the observations of camera sensors with overlapped coverage areas, which introduces substantial data redundancy in the network. In this dissertation, efficient communication schemes are designed for WMSNs by leveraging the correlation of visual information observed by camera sensors. First, a spatial correlation model is developed to estimate the correlation of visual information and the joint entropy of multiple correlated camera sensors. The compression performance of correlated visual information is then studied. An entropy-based divergence measure is proposed to predict the compression efficiency of performing joint coding on the images from correlated cameras. Based on the predicted compression efficiency, a clustered coding technique is proposed that maximizes the overall compression gain of the visual information gathered in WMSNs. The correlation of visual information is then utilized to design a network scheduling scheme to maximize the lifetime of WMSNs. Furthermore, as many WMSN applications require QoS support, a correlation-aware QoS routing algorithm is introduced that can efficiently deliver visual information under QoS constraints. Evaluation results show that, by utilizing the correlation of visual information in the communication process, the energy efficiency and networking performance of WMSNs could be improved significantly.

<p>La distribution quantique de clés est une technique cryptographique permettant l'échange de clés secrètes dont la confidentialité est garantie par les lois de la mécanique quantique. Le comportement particulier des particules élémentaires est exploité. En effet, en mécanique quantique, toute mesure sur l'état d'une particule modifie irrémédiablement cet état. En jouant sur cette propriété, deux parties, souvent appelées Alice et Bob, peuvent encoder une clé secrète dans des porteurs quantiques tels que des photons uniques. Toute tentative d'espionnage demande à l'espion, Eve, une mesure de l'état du photon qui transmet un bit de clé et donc se traduit par une perturbation de l'état. Alice et Bob peuvent alors se rendre compte de la présence d'Eve par un nombre inhabituel d'erreurs de transmission.</p><p><p><p>L'information échangée par la distribution quantique n'est pas directement utilisable mais doit être d'abord traitée. Les erreurs de transmissions, qu'elles soient dues à un espion ou simplement à du bruit dans le canal de communication, doivent être corrigées grâce à une technique appelée réconciliation. Ensuite, la connaissance partielle d'un espion qui n'aurait perturbé qu'une partie des porteurs doit être supprimée de la clé finale grâce à une technique dite d'amplification de confidentialité.</p><p><p><p>Cette thèse s'inscrit dans le contexte de la distribution quantique de clé où les porteurs sont des états continus de la lumière. En particulier, une partie importante de ce travail est consacrée au traitement de l'information continue échangée par un protocole particulier de distribution quantique de clés, où les porteurs sont des états cohérents de la lumière. La nature continue de cette information implique des aménagements particuliers des techniques de réconciliation, qui ont surtout été développées pour traiter l'information binaire. Nous proposons une technique dite de réconciliation en tranches qui permet de traiter efficacement l'information continue. L'ensemble des techniques développées a été utilisé en collaboration avec l'Institut d'Optique à Orsay, France, pour produire la première expérience de distribution quantique de clés au moyen d'états cohérents de la lumière modulés continuement.</p><p><p><p>D'autres aspects importants sont également traités dans cette thèse, tels que la mise en perspective de la distribution quantique de clés dans un contexte cryptographique, la spécification d'un protocole complet, la création de nouvelles techniques d'amplification de confidentialité plus rapides à mettre en œuvre ou l'étude théorique et pratique d'algorithmes alternatifs de réconciliation.</p><p><p><p>Enfin, nous étudions la sécurité du protocole à états cohérents en établissant son équivalence à un protocole de purification d'intrication. Sans entrer dans les détails, cette équivalence, formelle, permet de valider la robustesse du protocole contre tout type d'espionnage, même le plus compliqué possible, permis par les lois de la mécanique quantique. En particulier, nous généralisons l'algorithme de réconciliation en tranches pour le transformer en un protocole de purification et nous établissons ainsi un protocole de distribution quantique sûr contre toute stratégie d'espionnage.</p><p><p><p>Quantum key distribution is a cryptographic technique, which allows to exchange secret keys whose confidentiality is guaranteed by the laws of quantum mechanics. The strange behavior of elementary particles is exploited. In quantum mechnics, any measurement of the state of a particle irreversibly modifies this state. By taking advantage of this property, two parties, often called Alice and bob, can encode a secret key into quatum information carriers such as single photons. Any attempt at eavesdropping requires the spy, Eve, to measure the state of the photon and thus to perturb this state. Alice and Bob can then be aware of Eve's presence by a unusually high number of transmission errors.</p><p><p><p>The information exchanged by quantum key distribution is not directly usable but must first be processed. Transmission errors, whether they are caused by an eavesdropper or simply by noise in the transmission channel, must be corrected with a technique called reconciliation. Then, the partial knowledge of an eavesdropper, who would perturb only a fraction of the carriers, must be wiped out from the final key thanks to a technique called privacy amplification.</p><p><p><p>The context of this thesis is the quantum key distribution with continuous states of light as carriers. An important part of this work deals with the processing of continuous information exchanged by a particular protocol, where the carriers are coherent states of light. The continuous nature of information in this case implies peculiar changes to the reconciliation techniques, which have mostly been developed to process binary information. We propose a technique called sliced error correction, which allows to efficiently process continuous information. The set of the developed techniques was used in collaboration with the Institut d'Optique, Orsay, France, to set up the first experiment of quantum key distribution with continuously-modulated coherent states of light.</p><p><p><p>Other important aspects are also treated in this thesis, such as placing quantum key distribution in the context of a cryptosystem, the specification of a complete protocol, the creation of new techniques for faster privacy amplification or the theoretical and practical study of alternate reconciliation algorithms.</p><p><p><p>Finally, we study the security of the coherent state protocol by analyzing its equivalence with an entanglement purification protocol. Without going into the details, this formal equivalence allows to validate the robustness of the protocol against any kind of eavesdropping, even the most intricate one allowed by the laws of quantum mechanics. In particular, we generalize the sliced error correction algorithm so as to transform it into a purification protocol and we thus establish a quantum key distribution protocol secure against any eavesdropping strategy.</p> / Doctorat en sciences appliquées / info:eu-repo/semantics/nonPublished