Search

Recent advances in web technology have made in-browser crypto-mining a viable funding model. However, these services have been abused to launch large-scale cryptojacking attacks to secretly mine cryptocurrency in browsers. To detect them, various signature-based or runtime feature-based methods have been proposed. However, they can be imprecise or easily circumvented. To this end, we propose MinerRay, a generic scheme to detect malicious in-browser cryptominers. Instead of leveraging unreliable external patterns, MinerRay infers the essence of cryptomining behaviors that differentiate mining from common browser activities in both WebAssembly and JavaScript contexts. Additionally, to detect stealthy mining activities without user consents, MinerRay checks if the miner can only be instantiated from user actions. MinerRay was evaluated on over 1 million websites. It detected cryptominers on 901 websites, where 885 secretly start mining without user consent. Besides, we compared MinerRay with five state-of-the-art signature-based or behavior-based cryptominer detectors (MineSweeper, CMTracker, Outguard, No Coin, and minerBlock). We observed that emerging miners with new signatures or new services were detected by MinerRay but missed by others. The results show that our proposed technique is effective and robust in detecting evolving cryptominers, yielding more true positives, and fewer errors.

The sheer complexity of web applications leaves open a large attack surface of business logic. Particularly, in some scenarios, developers have to expose a portion of the logic to the client-side in order to coordinate multiple parties (e.g. merchants, client users, and third-party payment services) involved in a business process. However, such client-side code can be tampered with on the fly, leading to business logic perturbations and financial loss. Although developers become familiar with concepts that the client should never be trusted, given the size and the complexity of the client-side code that may be even incorporated from third parties, it is extremely challenging to understand and pinpoint the vulnerability. To this end, we investigate client-side business flow tampering vulnerabilities and develop a dynamic analysis based approach to automatically identifying such vulnerabilities. We evaluate our technique on 200 popular real-world websites. With negligible overhead, we have successfully identified 27 unique vulnerabilities on 23 websites, such as New York Times, HBO, and YouTube, where an adversary can interrupt business logic to bypass paywalls, disable adblocker detection, earn reward points illicitly, etc.

In recent years, string solvers have become an essential component in many formal verification, security analysis, and bug-finding tools. Such solvers typically support a theory of string equations, the length function, and the regular-expression membership predicate. These enable considerable expressive power, which comes at the cost of slow solving time, and in some cases even non-termination. We present three techniques, designed for word-based SMT string solvers, to mitigate these problems: (1) detecting overlapping variables, which is essential to avoiding common cases of non-termination; (2) pruning of the search space via bi-directional integration between the string and integer theories, enabling new cross-domain heuristics; and (3) a binary search based heuristic, allowing the procedure to skip unnecessary string length queries and converge on consistent length assignments faster for large strings. We have implemented above techniques atop the Z3-str solver, resulting in a significantly more robust and efficient solver, dubbed Z3str2, for the quantifier-free theory of string equations, the regular-expression membership predicate, and linear arithmetic over the length function. We report on a series of experiments over four sets of challenging real-world benchmarks, where we compare Z3str2 with five different string solvers: S3, CVC4, Kaluza, PISA and Stranger. Each of these tools utilizes a different solving strategy and/or string representation (based e.g. on words, bit vectors or automata). The results point to the efficacy of our proposed techniques, which yield dramatic performance improvement. We also demonstrate performance improvements enabled by Z3str2 in the context of symbolic execution for string-manipulating programs. We observe that the techniques presented here are of broad applicability, and can be integrated into other string solvers to improve their performance.

In this paper, we introduce StringFuzz: a modular SMT-LIB problem instance transformer and generator for string solvers. We supply a repository of instances generated by StringFuzz in SMT-LIB 2.0/2.5 format. We systematically compare Z3str3, CVC4, Z3str2, and Norn on groups of such instances, and identify those that are particularly challenging for some solvers. We briefly explain our observations and show how StringFuzz helped discover causes of performance degradations in Z3str3.

In this paper, we present a new ad budget draining attack. By repeatedly pulling ads from targeted advertisers using crafted browsing profiles, we are able to reduce the chance of showing their ads to real-human visitors and trash the ad budget. From the advertiser profiles collected by an automated crawler, we infer advertising strategies, train satisfying browsing profiles and launch large-scale attacks. We evaluate our methods on 291 public advertisers selected from Alexa Top 500, where we successfully reveal the targeting strategies used by 87% of the advertisers we considered. We also executed a series of attacks against a controlled advertiser and 3 real-world advertisers within the ethical and legal boundary. The results show that we are able to fetch 40,958 ads and drain up to $155.89 from the targeted advertisers within an hour.

In the current online advertisement delivery, an ad slot on a publisher's website may go through multiple layers of bidding and reselling until the final ad content is delivered. The publishers have little control on the ads being displayed on their web pages. As a result, website visitors may suffer from unwanted ads such as malvertising, intrusive ads, and information disclosure ads. Unfortunately, the visitors often blame the publisher for their unpleasant experience and switch to competitor websites. In this paper, we propose a novel programming support system for ad delivery, called PAD, for publisher programmers, who specify their policies on regulating third-party ads shown on their websites. PAD features an expressive specification language and a novel persistent policy enforcement runtime that can self-install and self-protect throughout the entire ad delegation chain. It also provides an ad-specific memory protection scheme that prevents malvertising by corrupting malicious payloads. Our experiments show that PAD has negligible runtime overhead. It effectively suppresses a set of malvertising cases and unwanted ad behaviors reported in the real world, without affecting normal functionalities and regular ads.

We present a new string SMT solver, Z3str3, that is faster than its competitors Z3str2, Norn, CVC4, S3, and S3P over a majority of three industrial-strength benchmarks, namely, Kaluza, PISA, and IBM AppScan. Z3str3 supports string equations, linear arithmetic over length function, and regular language membership predicate. The key algorithmic innovation behind the efficiency of Z3str3 is a technique we call theory-aware branching, wherein we modify Z3's branching heuristic to take into account the structure of theory literals to compute branching activities. In the traditional DPLL(T) architecture, the structure of theory literals is hidden from the DPLL(T) SAT solver because of the Boolean abstraction constructed over the input theory formula. By contrast, the theory-aware technique presented in this paper exposes the structure of theory literals to the DPLL(T) SAT solver's branching heuristic, thus enabling it to make much smarter decisions during its search than otherwise. As a consequence, Z3str3 has better performance than its competitors.

The rapid growth of Internet of Things (IoT) has been created a number of new platforms recently. Unfortunately, such variety of IoT devices causes platform fragmentation which makes software development on such devices challenging. In particular, existing programs cannot be simply reused on such devices as they rely on certain underlying hardware and software interfaces which we call platform dependencies. In this paper, we present CPR, a novel technique that synthesizes a platform independent program from a platform dependent program. Specifically, we leverage an existing system called PIEtrace which can generate a platform independent trace program. The generated trace program is platform independent while it can only reproduce a specific execution path. Hence, we develop an algorithm to merge a set of platform independent trace programs and synthesize a general program that can take multiple inputs. The synthesized platform-independent program is representative of the merged trace programs and the results produced by the program is correct if no exceptions occur. Our evaluation results on 15 real-world applications show that CPR is highly effective on reusing existing binaries across platforms.

Many designs have been proposed to improve the automated mobile testing. Despite these improvements, providing appropriate text inputs remains a prominent obstacle, which hinders the large-scale adoption of automated testing approaches. The key challenge is how to automatically produce the most relevant text in a use case context. For example, a valid website address should be entered in the address bar of a mobile browser app to continue the testing of the app, a singer's name should be entered in the search bar of a music recommendation app. Without the proper text inputs, the testing would get stuck. We propose a novel deep learning based approach to address the challenge, which reduces the problem to a minimization problem. Another challenge is how to make the approach generally applicable to both the trained apps and the untrained apps. We leverage the Word2Vec model to address the challenge. We have built our approaches as a tool and evaluated it with 50 iOS mobile apps including Firefox and Wikipedia. The results show that our approach significantly outperforms existing automatic text input generation methods.

Many JavaScript applications perform HTTP requests to web APIs, relying on the request URL, HTTP method, and request data to be constructed correctly by string operations. Traditional compile-time error checking, such as calling a non-existent method in Java, are not available for checking whether such requests comply with the requirements of a web API. In this paper, we propose an approach to statically check web API requests in JavaScript. Our approach first extracts a request's URL string, HTTP method, and the corresponding request data using an inter-procedural string analysis, and then checks whether the request conforms to given web API specifications. We evaluated our approach by checking whether web API requests in JavaScript files mined from GitHub are consistent or inconsistent with publicly available API specifications. From the 6575 requests in scope, our approach determined whether the request's URL and HTTP method was consistent or inconsistent with web API specifications with a precision of 96.0%. Our approach also correctly determined whether extracted request data was consistent or inconsistent with the data requirements with a precision of 87.9% for payload data and 99.9% for query data. In a systematic analysis of the inconsistent cases, we found that many of them were due to errors in the client code. The here proposed checker can be integrated with code editors or with continuous integration tools to warn programmers about code containing potentially erroneous requests., International Conference on Software Engineering, 2017

Web-based malware equipped with stealthy cloaking and obfuscation techniques is becoming more sophisticated nowadays. In this paper, we propose J-FORCE, a crash-free forced JavaScript execution engine to systematically explore possible execution paths and reveal malicious behaviors in such malware. In particular, J-FORCE records branch outcomes and mutates them for further explorations. J-FORCE inspects function parameter values that may reveal malicious intentions and expose suspicious DOM injections. We addressed a number of technical challenges encountered. For instance, we keep track of missing objects and DOM elements, and create them on demand. To verify the efficacy of our techniques, we apply J-FORCE to detect Exploit Kit (EK) attacks and malicious Chrome extensions. We observe that J-FORCE is more effective compared to the existing tools.

Nowadays, a rapidly increasing number of web users are using Ad-blockers to block online advertisements. Ad-blockers are browser-based software that can block most Ads on the websites, speeding up web browsers and saving bandwidth. Despite these benefits to end users, Ad-blockers could be catastrophic for the economic structure underlying the web, especially considering the rise of Ad-blocking as well as the number of technologies and services that rely exclusively on Ads to compensate their cost. In this paper, we introduce WebRanz that utilizes a randomization mechanism to circumvent Ad-blocking. Using WebRanz, content publishers can constantly mutate the internal HTML elements and element attributes of their web pages, without affecting their visual appearances and functionalities. Randomization invalidates the pre-defined patterns that Ad-blockers use to filter out Ads. Though the design of WebRanz is motivated by evading Ad-blockers, WebRanz also benefits the defense against bot scripts. We evaluate the effectiveness of WebRanz and its overhead using 221 randomly sampled top Alexa web pages and 8 representative bot scripts.

Modern browsers have a highly concurrent page rendering process in order to be more responsive. However, such a concurrent execution model leads to various race issues. In this paper, we present ARROW, a static technique that can automatically, safely, and cost effectively patch certain race issues on client side pages. It works by statically modeling a web page as a causal graph denoting happens-before relations between page elements, according to the rendering process in browsers. Races are detected by identifying inconsistencies between the graph and the dependence relations intended by the developer. Detected races are fixed by leveraging a constraint solver to add a set of edges with the minimum cost to the causal graph so that it is consistent with the intended dependences. The input page is then transformed to respect the repair edges. ARROW has fixed 151 races from 20 real world commercial web sites.

Integer overflow (IO) vulnerabilities can be exploited by attackers to compromise computer systems. In the mean time, IOs can be used intentionally by programmers for benign purposes such as hashing and random number generation. Hence, differentiating exploitable and harmful IOs from intentional and benign ones is an important challenge. It allows reducing the number of false positives produced by IO vulnerability detection techniques, helping developers or security analysts to focus on fixing critical IOs without inspecting the numerous false alarms. The difficulty of recognizing benign IOs mainly lies in inferring the intent of programmers from source code. In this paper, we present a novel technique to recognize benign IOs via equivalence checking across multiple precisions. We determine if an IO is benign by comparing the effects of an overflowed integer arithmetic operation in the actual world (with limited precision) and the same operation in the ideal world (with sufficient precision to evade the IO). Specifically, we first extract the data flow path from the overflowed integer arithmetic operation to a security-related program point (i.e., sink) and then create a new version of the path using more precise types with sufficient bits to represent integers so that the IO can be avoided. Using theorem proving we check whether these two versions are equivalent, that is, if they yield the same values at the sink under all possible inputs. If so, the IO is benign. We implement a prototype, named IntEQ, based on the GCC compiler and the Z3 solver, and evaluate it using 26 harmful IO vulnerabilities from 20 real-world programs, and 444 benign IOs from SPECINT 2000, SPECINT 2006, and 7 real-world applications. The experimental results show that IntEQ does not misclassify any harmful IO bugs (no false negatives) and recognizes 355 out of 444 (about 79.95%) benign IOs, whereas the state of the art can only recognize 19 benign IOs.

Deep learning (DL) training-as-a-service (TaaS) is an important emerging industrial workload. The unique challenge of TaaS is that it must satisfy a wide range of customers who have no experience and resources to tune DL hyper-parameters, and meticulous tuning for each user's dataset is prohibitively expensive. Therefore, TaaS hyper-parameters must be fixed with values that are applicable to all users. IBM Watson Natural Language Classifier (NLC) service, the most popular IBM cognitive service used by thousands of enterprise-level clients around the globe, is a typical TaaS service. By evaluating the NLC workloads, we show that only the conservative hyper-parameter setup (e.g., small mini-batch size and small learning rate) can guarantee acceptable model accuracy for a wide range of customers. We further justify theoretically why such a setup guarantees better model convergence in general. Unfortunately, the small mini-batch size causes a high volume of communication traffic in a parameter-server based system. We characterize the high communication bandwidth requirement of TaaS using representative industrial deep learning workloads and demonstrate that none of the state-of-the-art scale-up or scale-out solutions can satisfy such a requirement. We then present GaDei, an optimized shared-memory based scale-up parameter server design. We prove that the designed protocol is deadlock-free and it processes each gradient exactly once. Our implementation is evaluated on both commercial benchmarks and public benchmarks to demonstrate that it significantly outperforms the state-of-the-art parameter-server based implementation while maintaining the required accuracy and our implementation reaches near the best possible runtime performance, constrained only by the hardware limitation. Furthermore, to the best of our knowledge, GaDei is the only scale-up DL system that provides fault-tolerance.