OpenRaiser/Intern-Atlas huggingface dataset:
eThor: Practical and Provably Sound Static Analysis of Ethereum Smart Contracts
Venue: arXiv cs.PL 2020
Year: 2020

Ethereum has emerged as the most popular smart contract development platform, with hundreds of thousands of contracts stored on the blockchain and covering a variety of application scenarios, such as auctions, trading platforms, and so on. Given their financial nature, security vulnerabilities may lead to catastrophic consequences and, even worse, they can be hardly fixed as data stored on the blockchain, including the smart contract code itself, are immutable. An automated security analysis of these contracts is thus of utmost interest, but at the same time technically challenging for a variety of reasons, such as the specific transaction-oriented programming mechanisms, which feature a subtle semantics, and the fact that the blockchain data which the contract under analysis interacts with, including the code of callers and callees, are not statically known. In this work, we present eThor, the first sound and automated static analyzer for EVM bytecode, which is based on an abstraction of the EVM bytecode semantics based on Horn clauses. In particular, our static analysis supports reachability properties, which we show to be sufficient for capturing interesting security properties for smart contracts (e.g., single-entrancy) as well as contract-specific functional properties. Our analysis is proven sound against a complete semantics of EVM bytecode and an experimental large-scale evaluation on real-world contracts demonstrates that eThor is practical and outperforms the state-of-the-art static analyzers: specifically, eThor is the only one to provide soundness guarantees, terminates on 95% of a representative set of real-world contracts, and achieves an F-measure (which combines sensitivity and specificity) of 89%.
Explainable Reinforcement Learning: A Survey
Venue: arXiv cs.LG 2020
Year: 2020

Explainable Artificial Intelligence (XAI), i.e., the development of more transparent and interpretable AI models, has gained increased traction over the last few years. This is due to the fact that, in conjunction with their growth into powerful and ubiquitous tools, AI models exhibit one detrimential characteristic: a performance-transparency trade-off. This describes the fact that the more complex a model's inner workings, the less clear it is how its predictions or decisions were achieved. But, especially considering Machine Learning (ML) methods like Reinforcement Learning (RL) where the system learns autonomously, the necessity to understand the underlying reasoning for their decisions becomes apparent. Since, to the best of our knowledge, there exists no single work offering an overview of Explainable Reinforcement Learning (XRL) methods, this survey attempts to address this gap. We give a short summary of the problem, a definition of important terms, and offer a classification and assessment of current XRL methods. We found that a) the majority of XRL methods function by mimicking and simplifying a complex model instead of designing an inherently simple one, and b) XRL (and XAI) methods often neglect to consider the human side of the equation, not taking into account research from related fields like psychology or philosophy. Thus, an interdisciplinary effort is needed to adapt the generated explanations to a (non-expert) human user in order to effectively progress in the field of XRL and XAI in general.
MeSH descriptors indicate the knowledge growth in the SARS-CoV-2/COVID-19 pandemic
Venue: arXiv cs.DL 2020
Year: 2020

The scientific papers dealing with the novel betacoronavirus SARS-CoV-2 and the coronavirus disease 2019 (COVID-19) caused by this virus, published in 2020 and recorded in the database PUBMED, were retrieved on April 27, 2020. About 20\% of the records contain Medical Subject Headings (MeSH), keywords assigned to records in the course of the indexing process in order to summarise the articles' contents. The temporal sequence of the first occurrences of the keywords was determined, thus giving insight into the growth of the knowledge base of the pandemic.
Failure Mode Reasoning in Model Based Safety Analysis
Venue: arXiv cs.SE 2020
Year: 2020

Failure Mode Reasoning (FMR) is a novel approach for analyzing failure in a Safety Instrumented System (SIS). The method uses an automatic analysis of an SIS program to calculate potential failures in parts of the SIS. In this paper we use a case study from the power industry to demonstrate how FMR can be utilized in conjunction with other model-based safety analysis methods, such as HiP-HOPS and CFT, in order to achieve a comprehensive safety analysis of SIS. In this case study, FMR covers the analysis of SIS inputs while HiP-HOPS/CFT models the faults of logic solver and final elements. The SIS program is analyzed by FMR and the results are exported to HiP-HOPS/CFT via automated interfaces. The final outcome is the collective list of SIS failure modes along with their reliability measures. We present and review the results from both qualitative and quantitative perspectives.
Some Model Theory of Guarded Negation
Venue: arXiv cs.LO 2020
Year: 2020

The Guarded Negation Fragment (GNFO) is a fragment of first-order logic that contains all positive existential formulas, can express the first-order translations of basic modal logic and of many description logics, along with many sentences that arise in databases. It has been shown that the syntax of GNFO is restrictive enough so that computational problems such as validity and satisfiability are still decidable. This suggests that, in spite of its expressive power, GNFO formulas are amenable to novel optimizations. In this paper we study the model theory of GNFO formulas. Our results include effective preservation theorems for GNFO, effective Craig Interpolation and Beth Definability results, and the ability to express the certain answers of queries with respect to a large class of GNFO sentences within very restricted logics. This version of the paper contains streamlined and corrected versions of results concerning entailment of a conjunctive query from a set of ground facts and a theory consisting of GNFO sentences of a special form ("dependencies").
LeviCursor: Dexterous Interaction with a Levitating Object
Venue: arXiv cs.HC 2020
Year: 2020

We present LeviCursor, a method for interactively moving a physical, levitating particle in 3D with high agility. The levitating object can move continuously and smoothly in any direction. We optimize the transducer phases for each possible levitation point independently. Using precomputation, our system can determine the optimal transducer phases within a few microseconds and achieves round-trip latencies of 15 ms. Due to our interpolation scheme, the levitated object can be controlled almost instantaneously with sub-millimeter accuracy. We present a particle stabilization mechanism which ensures the levitating particle is always in the main levitation trap. Lastly, we conduct the first Fitts' law-type pointing study with a real 3D cursor, where participants control the movement of the levitated cursor between two physical targets. The results of the user study demonstrate that using LeviCursor, users reach performance comparable to that of a mouse pointer.
Oblivion of Online Reputation: How Time Cues Improve Online Recruitment
Venue: arXiv cs.CY 2020
Year: 2020

In online crowdsourcing labour markets, employers decide which job-seekers to hire based on their reputation profiles. If reputation systems neglect the aspect of time when displaying reputation profiles, though, employers risk taking false decisions, deeming an obsolete reputation to be still relevant. As a consequence, job-seekers might be unwarrantedly deprived of getting hired for new jobs and can be harmed in their professional careers in the long-run. This paper argues that exposing employers to the temporal context of job-seekers' reputation leads to better hiring decisions. The visible temporal context in reputation systems helps employers to ignore a job-seeker's obsolete reputation. An experimental lab study with 335 students shows that current reputation systems fall short of making them aware of obsolete reputation. In contrast, graphical time cues improve the social efficiency of hiring decisions.
Stealth Communication with Vanishing Power over Binary Symmetric Channels
Venue: arXiv cs.IT 2020
Year: 2020

A framework for stealth communication with vanishing power (VP) is presented by studying binary symmetric channels. Coding theorems are proved by modifying Gallager's error exponents for VP and by applying resolvability exponents. The analysis unifies and generalizes existing rate bounds for covert and stealth communication.
k-Approximate Quasiperiodicity under Hamming and Edit Distance
Venue: arXiv cs.DS 2020
Year: 2020

Quasiperiodicity in strings was introduced almost 30 years ago as an extension of string periodicity. The basic notions of quasiperiodicity are cover and seed. A cover of a text $T$ is a string whose occurrences in $T$ cover all positions of $T$. A seed of text $T$ is a cover of a superstring of $T$. In various applications exact quasiperiodicity is still not sufficient due to the presence of errors. We consider approximate notions of quasiperiodicity, for which we allow approximate occurrences in $T$ with a small Hamming, Levenshtein or weighted edit distance. In previous work Sip et al. (2002) and Christodoulakis et al. (2005) showed that computing approximate covers and seeds, respectively, under weighted edit distance is NP-hard. They, therefore, considered restricted approximate covers and seeds which need to be factors of the original string $T$ and presented polynomial-time algorithms for computing them. Further algorithms, considering approximate occurrences with Hamming distance bounded by $k$, were given in several contributions by Guth et al. They also studied relaxed approximate quasiperiods that do not need to cover all positions of $T$. In case of large data the exponents in polynomial time complexity play a crucial role. We present more efficient algorithms for computing restricted approximate covers and seeds. In particular, we improve upon the complexities of many of the aforementioned algorithms, also for relaxed quasiperiods. Our solutions are especially efficient if the number (or total cost) of allowed errors is bounded. We also show NP-hardness of computing non-restricted approximate covers and seeds under Hamming distance. Approximate covers were studied in three recent contributions at CPM over the last three years. However, these works consider a different definition of an approximate cover of $T$.
Progressive growing of self-organized hierarchical representations for exploration
Venue: arXiv cs.LG 2020
Year: 2020

Designing agent that can autonomously discover and learn a diversity of structures and skills in unknown changing environments is key for lifelong machine learning. A central challenge is how to learn incrementally representations in order to progressively build a map of the discovered structures and re-use it to further explore. To address this challenge, we identify and target several key functionalities. First, we aim to build lasting representations and avoid catastrophic forgetting throughout the exploration process. Secondly we aim to learn a diversity of representations allowing to discover a "diversity of diversity" of structures (and associated skills) in complex high-dimensional environments. Thirdly, we target representations that can structure the agent discoveries in a coarse-to-fine manner. Finally, we target the reuse of such representations to drive exploration toward an "interesting" type of diversity, for instance leveraging human guidance. Current approaches in state representation learning rely generally on monolithic architectures which do not enable all these functionalities. Therefore, we present a novel technique to progressively construct a Hierarchy of Observation Latent Models for Exploration Stratification, called HOLMES. This technique couples the use of a dynamic modular model architecture for representation learning with intrinsically-motivated goal exploration processes (IMGEPs). The paper shows results in the domain of automated discovery of diverse self-organized patterns, considering as testbed the experimental framework from Reinke et al. (2019).
Dyslexia and Dysgraphia prediction: A new machine learning approach
Venue: arXiv cs.OH 2020
Year: 2020

Learning disabilities like dysgraphia, dyslexia, dyspraxia, etc. interfere with academic achievements but have also long terms consequences beyond the academic time. It is widely admitted that between 5% to 10% of the world population is subject to this kind of disabilities. For assessing such disabilities in early childhood, children have to solve a battery of tests. Human experts score these tests, and decide whether the children require specific education strategy on the basis of their marks. The assessment can be lengthy, costly and emotionally painful. In this paper, we investigate how Artificial Intelligence can help in automating this assessment. Gathering a dataset of handwritten text pictures and audio recordings, both from standard children and from dyslexic and/or dysgraphic children, we apply machine learning techniques for classification in order to analyze the differences between dyslexic/dysgraphic and standard readers/writers and to build a model. The model is trained on simple features obtained by analysing the pictures and the audio files. Our preliminary implementation shows relatively high performances on the dataset we have used. This suggests the possibility to screen dyslexia and dysgraphia via non-invasive methods in an accurate way as soon as enough data are available.
Designing a Color Filter via Optimization of Vora-Value for Making a Camera more Colorimetric
Venue: arXiv cs.CV 2020
Year: 2020

The Luther condition states that if the spectral sensitivity responses of a camera are a linear transform from the color matching functions of the human visual system, the camera is colorimetric. Previous work proposed to solve for a filter which, when placed in front of a camera, results in sensitivities that best satisfy the Luther condition. By construction, the prior art solves for a filter for a given set of human visual sensitivities, e.g. the XYZ color matching functions or the cone response functions. However, depending on the target spectral sensitivity set, a different optimal filter is found. This paper begins with the observation that the cone fundamentals, XYZ color matching functions or any linear combination thereof span the same 3-dimensional subspace. Thus, we set out to solve for a filter that makes the vector space spanned by the filtered camera sensitivities as similar as possible to the space spanned by human vision sensors. We argue that the Vora-Value is a suitable way to measure subspace similarity and we develop an optimization method for finding a filter that maximizes the Vora-Value measure. Experiments demonstrate that our new optimization leads to filtered camera sensitivities which have a significantly higher Vora-Value compared with antecedent methods.
Testing Positive Semi-Definiteness via Random Submatrices
Venue: arXiv cs.DS 2020
Year: 2020

We study the problem of testing whether a matrix $\mathbf{A} \in \mathbb{R}^{n \times n}$ with bounded entries ($\|\mathbf{A}\|_\infty \leq 1$) is positive semi-definite (PSD), or $ε$-far in Euclidean distance from the PSD cone, meaning that $\min_{\mathbf{B} \succeq 0} \|\mathbf{A} - \mathbf{B}\|_F^2 > εn^2$, where $\mathbf{B} \succeq 0$ denotes that $\mathbf{B}$ is PSD. Our main algorithmic contribution is a non-adaptive tester which distinguishes between these cases using only $\tilde{O}(1/ε^4)$ queries to the entries of $\mathbf{A}$. If instead of the Euclidean norm we considered the distance in spectral norm, we obtain the "$\ell_\infty$-gap problem", where $\mathbf{A}$ is either PSD or satisfies $\min_{\mathbf{B}\succeq 0} \|\mathbf{A}- \mathbf{B}\|_2 > εn$. For this related problem, we give a $\tilde{O}(1/ε^2)$ query tester, which we show is optimal up to $\log(1/ε)$ factors. Our testers randomly sample a collection of principal submatrices and check whether these submatrices are PSD. Consequentially, our algorithms achieve one-sided error: whenever they output that $\mathbf{A}$ is not PSD, they return a certificate that $\mathbf{A}$ has negative eigenvalues. We complement our upper bound for PSD testing with Euclidean norm distance by giving a $\tildeΩ(1/ε^2)$ lower bound for any non-adaptive algorithm. Our lower bound construction is general, and can be used to derive lower bounds for a number of spectral testing problems. As an example of the applicability of our construction, we obtain a new $\tildeΩ(1/ε^4)$ sampling lower bound for testing the Schatten-$1$ norm with a $εn^{1.5}$ gap, extending a result of Balcan, Li, Woodruff, and Zhang [SODA'19]. In addition, it yields new sampling lower bounds for estimating the Ky-Fan Norm, and the cost of the best rank-$k$ approximation.
Representing Whole Slide Cancer Image Features with Hilbert Curves
Venue: arXiv cs.GR 2020
Year: 2020

Regions of Interest (ROI) contain morphological features in pathology whole slide images (WSI) are delimited with polygons[1]. These polygons are often represented in either a textual notation (with the array of edges) or in a binary mask form. Textual notations have an advantage of human readability and portability, whereas, binary mask representations are more useful as the input and output of feature-extraction pipelines that employ deep learning methodologies. For any given whole slide image, more than a million cellular features can be segmented generating a corresponding number of polygons. The corpus of these segmentations for all processed whole slide images creates various challenges for filtering specific areas of data for use in interactive real-time and multi-scale displays and analysis. Simple range queries of image locations do not scale and, instead, spatial indexing schemes are required. In this paper we propose using Hilbert Curves simultaneously for spatial indexing and as a polygonal ROI representation. This is achieved by using a series of Hilbert Curves[2] creating an efficient and inherently spatially-indexed machine-usable form. The distinctive property of Hilbert curves that enables both mask and polygon delimitation of ROIs is that the elements of the vector extracted ro describe morphological features maintain their relative positions for different scales of the same image.
Modeling Human Dynamics and Lifestyle Using Digital Traces
Venue: arXiv cs.SI 2020
Year: 2020

Human behavior drives a range of complex social, urban, and economic systems, yet understanding its structure and dynamics at the individual level remains an open question. From credit card transactions to communications data, human behavior appears to exhibit bursts of activity driven by task prioritization and periodicity, however, current research does not offer generative models capturing these mechanisms. We propose a multivariate, periodic Hawkes process (MPHP) model that captures -- at the individual level -- the temporal clustering of human activity, the interdependence structure and co-excitation of different activities, and the periodic effects of weekly rhythms. We also propose a scalable parameter estimation technique for this model using maximum-aposteriori expectation-maximization that additionally provides estimation of latent variables revealing branching structure of an individual's behavior patterns. We apply the model to a large dataset of credit card transactions, and demonstrate the MPHP outperforms a non-homogeneous Poisson model and LDA in both statistical fit for the distribution of inter-event times and an activity prediction task.
Russian trolls speaking Russian: Regional Twitter operations and MH17
Venue: arXiv cs.SI 2020
Year: 2020

The role of social media in promoting media pluralism was initially viewed as wholly positive. However, some governments are allegedly manipulating social media by hiring online commentators (also known as trolls) to spread propaganda and disinformation. In particular, an alleged system of professional trolls operating both domestically and internationally exists in Russia. In 2018, Twitter released data on accounts identified as Russian trolls, starting a wave of research. However, while foreign-targeted English language operations of these trolls have received significant attention, no research has analyzed their Russian language domestic and regional-targeted activities. We address this gap by characterizing the Russian-language operations of Russian trolls. We first perform a descriptive analysis, and then focus in on the trolls' operation related to the crash of Malaysia Airlines flight MH17. Among other things, we find that Russian-language trolls have run 163 hashtag campaigns (where hashtag use grows abruptly within a month). The main political sentiments of such campaigns were praising Russia and Putin (29%), criticizing Ukraine (26%), and criticizing the United States and Obama (9%). Further, trolls actively reshared information with 76% of tweets being retweets or containing a URL. Additionally, we observe periodic temporal patterns of tweeting suggesting that trolls use automation tools. Further, we find that trolls' information campaign on the MH17 crash was the largest in terms of tweet count. However, around 68% of tweets posted with MH17 hashtags were likely used simply for hashtag amplification. With these tweets excluded, about 49% of the tweets suggested to varying levels that Ukraine was responsible for the crash, and only 13% contained disinformation and propaganda presented as news. Interestingly, trolls promoted inconsistent alternative theories for the crash.
Phishing URL Detection Through Top-level Domain Analysis: A Descriptive Approach
Venue: arXiv cs.CR 2020
Year: 2020

Phishing is considered to be one of the most prevalent cyber-attacks because of its immense flexibility and alarmingly high success rate. Even with adequate training and high situational awareness, it can still be hard for users to continually be aware of the URL of the website they are visiting. Traditional detection methods rely on blocklists and content analysis, both of which require time-consuming human verification. Thus, there have been attempts focusing on the predictive filtering of such URLs. This study aims to develop a machine-learning model to detect fraudulent URLs which can be used within the Splunk platform. Inspired from similar approaches in the literature, we trained the SVM and Random Forests algorithms using malicious and benign datasets found in the literature and one dataset that we created. We evaluated the algorithms' performance with precision and recall, reaching up to 85% precision and 87% recall in the case of Random Forests while SVM achieved up to 90% precision and 88% recall using only descriptive features.
Cyberbullying Detection with Fairness Constraints
Venue: arXiv cs.CL 2020
Year: 2020

Cyberbullying is a widespread adverse phenomenon among online social interactions in today's digital society. While numerous computational studies focus on enhancing the cyberbullying detection performance of machine learning algorithms, proposed models tend to carry and reinforce unintended social biases. In this study, we try to answer the research question of "Can we mitigate the unintended bias of cyberbullying detection models by guiding the model training with fairness constraints?". For this purpose, we propose a model training scheme that can employ fairness constraints and validate our approach with different datasets. We demonstrate that various types of unintended biases can be successfully mitigated without impairing the model quality. We believe our work contributes to the pursuit of unbiased, transparent, and ethical machine learning solutions for cyber-social health.