Biblio

We describe a (time) cost model for the (call-by-value) λ-calculus based on a natural presentation of its game semantics: the cost of computing a finite approximant to the denotation of a term (its evaluation tree) is the size of its smallest derivation in the semantics. This measure has an optimality property enabling compositional reasoning about cost bounds: for any term A, context C[\_] and approximants a and c to the trees of A and C[A], the cost of computing c from C[A] is no more than the cost of computing a from A and c from C[a].Although the natural semantics on which it is based is nondeterministic, our cost model is reasonable: we describe a deterministic algorithm for recognizing evaluation tree approximants which satisfies it (up to a constant factor overhead) on a Random Access Machine. This requires an implementation of the λv-calculus on the RAM which is completely lazy: compositionality of costs entails that work done to evaluate any part of a term cannot be duplicated. This is achieved by a novel implementation of graph reduction for nameless explicit substitutions, to which we compile the λv-calculus via a series of linear cost reductions.

Nowadays, children, teens, and almost everyone around us tend to receive abundant and frequent advice regarding the usefulness of syllabification. Not only does it improve pronunciation, but it also makes it easier for us to read unfamiliar words in chunks of syllables rather than reading them all at once. Within this paper, we have designed, implemented, and presented a Turing machine-based syllable splitter. A Turing machine forms the theoretical basis for all modern computers and can be used to solve universal problems. On the other hand, a syllable splitter is used to hyphenate words into their corresponding syllables. We have proposed our work by illustrating the various states of the Turing machine, along with the rules it abides by, its machine specifications, and transition function. In addition to this, we have implemented a Graphical User Interface to stimulate our Turing machine to analyze our results better.

Wireless communication systems are inherently vulnerable to adversarial attacks since malevolent jammers might jam and disrupt the legitimate transmission intentionally. Of particular interest are so- called denial-of-service (DoS) attacks in which the jammer is able to completely disrupt the communication. Accordingly, it is of crucial interest for the legitimate users to detect such DoS attacks. Turing machines provide the fundamental limits of today's digital computers and therewith of the traditional signal processing. It has been shown that these are incapable of detecting DoS attacks. This stimulates the question of how powerful the signal processing must be to enable the detection of DoS attacks. This paper investigates the general computation framework of Blum-Shub-Smale machines which allows the processing and storage of arbitrary reals. It is shown that such real number signal processing then enables the detection of DoS attacks.

The wide-spread adoption of system defenses such as the randomization of code, stack, and heap raises the bar for code-reuse attacks. Thus, attackers utilize a scripting engine in target programs like a web browser to prepare the code-reuse chain, e.g., relocate gadget addresses or perform a just-in-time gadget search. However, many types of programs do not provide such an execution context that an attacker can use. Recent advances in data-oriented programming (DOP) explored an orthogonal way to abuse memory corruption vulnerabilities and demonstrated that an attacker can achieve Turing-complete computations without modifying code pointers in applications. As of now, constructing DOP exploits requires a lot of manual work-for every combination of application and payload anew. In this paper, we present novel techniques to automate the process of generating DOP exploits. We implemented a compiler called STEROIDS that leverages these techniques and compiles our high-level language SLANG into low-level DOP data structures driving malicious computations at run time. This enables an attacker to specify her intent in an application-and vulnerability-independent manner to maximize reusability. We demonstrate the effectiveness of our techniques and prototype implementation by specifying four programs of varying complexity in SLANG that calculate the Levenshtein distance, traverse a pointer chain to steal a private key, relocate a ROP chain, and perform a JIT-ROP attack. STEROIDS compiles each of those programs to low-level DOP data structures targeted at five different applications including GStreamer, Wireshark and ProFTPd, which have vastly different vulnerabilities and DOP instances. Ultimately, this shows that our compiler is versatile, can be used for both 32-bit and 64-bit applications, works across bug classes, and enables highly expressive attacks without conventional code-injection or code-reuse techniques in applications lacking a scripting engine.

Advances in our understanding of the nature of cognition in its myriad forms (Embodied, Embedded, Extended, and Enactive) displayed in all living beings (cellular organisms, animals, plants, and humans) and new theories of information, info-computation and knowledge are throwing light on how we should build software systems in the digital universe which mimic and interact with intelligent, sentient and resilient beings in the physical universe. Recent attempts to infuse cognition into computing systems to push the boundaries of Church-Turing thesis have led to new computing models that mimic biological systems in encoding knowledge structures using both algorithms executed in stored program control machines and neural networks. This paper presents a new model and implements an application as hierarchical named network composed of microservices to create a managed process workflow by enabling dynamic configuration and reconfiguration of the microservice network. We demonstrate the resiliency, efficiency and scaling of the named microservice network using a novel edge cloud platform by Platina Systems. The platform eliminates the need for Virtual Machine overlay and provides high performance and low-latency with L3 based 100 GbE network and SSD support with RDMA and NVMeoE. The hierarchical named microservice network using Kubernetes provisioning stack provides all the cloud features such as elasticity, autoscaling, self-repair and live-migration without reboot. The model is derived from a recent theoretical framework for unification of different models of computation using "Structural Machines.'' They are shown to simulate Turing machines, inductive Turing machines and also are proved to be more efficient than Turing machines. The structural machine framework with a hierarchy of controllers managing the named service connections provides dynamic reconfiguration of the service network from browsers to database to address rapid fluctuations in the demand for or the availability of resources without having to reconfigure IP address base networks.

We set up a framework for the formal proofs of RFID protocols in the computational model. We rely on the so-called computationally complete symbolic attacker model. Our contributions are: 1) to design (and prove sound) axioms reflecting the properties of hash functions (Collision-Resistance, PRF). 2) to formalize computational unlinkability in the model. 3) to illustrate the method, providing the first formal proofs of unlinkability of RFID protocols, in the omputational model.