Biblio
With the development of the information age, the process of global networking continues to deepen, and the cyberspace security has become an important support for today’s social functions and social activities. Web applications which have many security risks are the most direct interactive way in the process of the Internet activities. That is why the web applications face a large number of network attacks. Interpretive dynamic programming languages are easy to lean and convenient to use, they are widely used in the development of cross-platform web systems. As well as benefit from these advantages, the web system based on those languages is hard to detect errors and maintain the complex system logic, increasing the risk of system vulnerability and cyber threats. The attack defense of systems based on interpretive dynamic programming languages is widely concerned by researchers. Since the advance of endogenous security technologies, there are breakthroughs on the research of web system security. Compared with traditional security defense technologies, these technologies protect the system with their uncertainty, randomness and dynamism. Based on several common network attacks, the traditional system security defense technology and endogenous security technology of web application based on interpretive dynamic languages are surveyed and compared in this paper. Furthermore, the possible research directions of those technologies are discussed.
In this work, we consider the application of the nonstationary channel polarization theory on the wiretap channel model with non-stationary blocks. Particularly, we present a time-bit coding scheme which is a secure polar codes that constructed on the virtual bit blocks by using the non-stationary channel polarization theory. We have proven that this time-bit coding scheme achieves reliability, strong security and the secrecy capacity. Also, compared with regular secure polar coding methods, our scheme has a lower coding complexity for non-stationary channel blocks.
Proving secure compilation of partial programs typically requires back-translating an attack against the compiled program to an attack against the source program. To prove back-translation, one can syntactically translate the target attacker to a source one-i.e., syntax-directed back-translation-or show that the interaction traces of the target attacker can also be emitted by source attackers—i.e., trace-directed back-translation. Syntax-directed back-translation is not suitable when the target attacker may use unstructured control flow that the source language cannot directly represent. Trace-directed back-translation works with such syntactic dissimilarity because only the external interactions of the target attacker have to be mimicked in the source, not its internal control flow. Revealing only external interactions is, however, inconvenient when sharing memory via unforgeable pointers, since information about shared pointers stashed in private memory is not present on the trace. This made prior proofs unnecessarily complex, since the generated attacker had to instead stash all reachable pointers. In this work, we introduce more informative data-flow traces, combining the best of syntax- and trace-directed back-translation in a simpler technique that handles both syntactic dissimilarity and memory sharing well, and that is proved correct in Coq. Additionally, we develop a novel turn-taking simulation relation and use it to prove a recomposition lemma, which is key to reusing compiler correctness in such secure compilation proofs. We are the first to mechanize such a recomposition lemma in the presence of memory sharing. We use these two innovations in a secure compilation proof for a code generation compiler pass between a source language with structured control flow and a target language with unstructured control flow, both with safe pointers and components.