Search for: All records

Machine learning accelerators (MLAs) are increasingly im- portant in many applications such as image and video processing, speech recognition, and natural language processing. To achieve the needed per- formances and power efficiencies, MLAs are highly concurrent. The cor- rectness of MLAs hinges on the concept of sequential consistency, i.e., the concurrent execution of a program by an MLA must be equivalent to a sequential execution of the program. In this paper, we certify the sequential consistency of modular MLAs using theorem proving. We őrst provide a formalization of the MLAs and deőne their sequential consis- tency. After that, we introduce our certiőcation methodology based on inductive theorem proving. Finally, we demonstrate the feasibility of our approach through the analysis of the NVIDIA Deep Learning Accelerator and the Versatile Tensor Accelerator 

JavaScript has become the most popular programming language for web front-end development. With such popularity, there is a great demand for thorough testing of client-side JavaScript web applications. In this paper, we present a novel approach to concolic testing of front-end JavaScript web applications. This approach leverages widely used JavaScript testing frameworks such as Jest and Puppeteer and conducts concolic execution on JavaScript functions in web applications for unit testing. The seamless integration of concolic testing with these testing frameworks allows injection of symbolic variables within the native execution context of a JavaScript web function and precise capture of concrete execution traces of the function under test. Such concise execution traces greatly improve the effectiveness and efficiency of the subsequent symbolic analysis for test generation. We have implemented our approach on Jest and Puppeteer. The application of our Jest implementation on Metamask, one of the most popular Crypto wallets, has uncovered 3 bugs and 1 test suite improvement, whose bug reports have all been accepted by Metamask developers on Github. We also applied our Puppeteer implementation to 21 Github projects and detected 4 bugs. 

JavaScript (JS) has evolved into a versatile and popular programming language for not only the web, but also a wide range of server-side and client-side applications. Effective, efficient, and easy-to-use testing techniques for JS scripts are in great demand. In this paper, we introduce a holistic approach to applying concolic testing to JS scripts in-situ, i.e., JS scripts are executed in their native environments as part of concolic execution and test cases generated are directly replayed in these environments. We have implemented this approach in the context of Node.js, a JS runtime built on top of Chrome’s V8 JS engine, and evaluated its effectiveness and efficiency through application to 180 Node.js libraries with heavy use of string operations. For 85% of these libraries, it achieved statement coverage ranging between 75% and 100%, a close match in coverage with the hand-crafted unit test suites accompanying their NPM releases. Our approach detected numerous exceptions in these libraries. We analyzed the exception reports for 12 representative libraries and found 6 bugs in these libraries, 4 of which are previously undetected. The bug reports and patches that we filed for these bugs have been accepted by the library developers on GitHub. 

Attackers rely upon a vast array of tools for automating attacksagainst vulnerable servers and services. It is often the case thatwhen vulnerabilities are disclosed, scripts for detecting and exploit-ing them in tools such asNmapandMetasploitare released soonafter, leading to the immediate identification and compromise ofvulnerable systems. Honeypots, honeynets, tarpits, and other decep-tive techniques can be used to slow attackers down, however, such approaches have difficulty keeping up with the sheer number of vulnerabilities being discovered and attacking scripts that are being released. To address this issue, this paper describes an approach for applying concolic execution on attacking scripts in Nmap in order to automatically generate lightweight fake versions of the vulnerable services that can fool the scripts. By doing so in an automated and scalable manner, the approach can enable rapid deployment of custom honeyfarms that leverage the results of concolic execution to trick an attacker's script into returning a result chosen by the honeyfarm, making the script unreliable for the use by the attacker. 

Paleomagnetic, rock magnetic, or geomagnetic data found in the MagIC data repository from a paper titled: New archaeomagnetic direction results from China and their constraints on palaeosecular variation of the geomagnetic field in Eastern Asia 

Abstract How astrophysical systems translate the kinetic energy of bulk motion into the acceleration of particles to very high energies is a pressing question. SS 433 is a microquasar that emits TeVγ-rays indicating the presence of high-energy particles. A region of hard X-ray emission in the eastern lobe of SS 433 was recently identified as an acceleration site. We observed this region with the Imaging X-ray Polarimetry Explorer and measured a polarization degree in the range 38%–77%. The high polarization degree indicates the magnetic field has a well-ordered component if the X-rays are due to synchrotron emission. The polarization angle is in the range −12° to +10° (east of north), which indicates that the magnetic field is parallel to the jet. Magnetic fields parallel to the bulk flow have also been found in supernova remnants and the jets of powerful radio galaxies. This may be caused by interaction of the flow with the ambient medium.