dataesr/scientific-paragraphs-categorization huggingface dataset:
A technique that scales well on binary code and that naturally comes into play for bug-finding and bounded-verification is symbolic execution (SE)  [3, 37]. While it has proven very successful for standard safety properties  [38] , its direct adaptation to 2-hypersafety properties through (variants of) self-composition suffers from a scalability issue  [39, 40, 41]. Some recent approaches scale better, but at the cost of sacrificing either bounded-verification  [27, 42]  (by doing under-approximations) or bug-finding  [23]  (by doing over-approximations). The idea of analyzing pairs of executions for the verification of 2-hypersafety is not new (e. g. relational Hoare logic  [43] , self-composition  [33] , product programs  [44] , multiple facets  [45, 46] ). In the context of symbolic execution, it has first been coined as ShadowSE  [47]  for back-to-back testing, and later as relational symbolic execution (RelSE)  [48].
Lucky13  [50] ) and automatically generate counterexamples (Section 6. 1); • Simon et al. [15]  have demonstrated that clang's optimizations break constant-timeness of code. We extend this work in five directions-from 192 in  [15]  to 4148 configurations (Section 6. 2):  (1)  we automatically analyze the code that was manually checked in  [15] ,  (2)  we add new implementations, (3) we add the gcc compiler and a more recent version of clang, (4) we add i686 and ARM,  (5)  we investigate the impact of individual optimizations-i. e. , the -x86-cmov-converter of clang and the if-conversion passes of gcc. Interestingly, we discovered that gcc -O0 and backend passes of clang introduce violations of constant-time that cannot be detected by LLVM verification tools like ct-verif  [22]  even when the -x86-cmov-converter is disabled.
Availability. We made Binsec/Rel open-source at https://github. com/binsec/rel, our experiments are available at https://github. com/binsec/rel_bench, and in particular, our studies on the preservation of constant-time and secreterasure by compilers are available at https://github. com/binsec/rel_bench/tree/main/properties_vs_compilers. Extension of article  [51]. This paper is an extension of the article Binsec/Rel: Efficient Relational Symbolic Execution for Constant-Time at Binary-Level  [51] , with the following additional contributions: • The leakage model considered in  [51]  restricts to constant-time while this work encompasses a more general subset of information flow properties. In particular, we define a new leakage model and property to capture the notion of secret-erasure (cf.
Relational Symbolic Execution (RelSE) RelSE improves over self-composition by maximizing sharing between the pairs of executions  [47, 48]  a pair of expressions, its result will be a pair of expressions. This representation offers two main advantages. First, this enables sharing redundant parts of  and  ′ , reducing the size of the self-composed formula. Second, variables mapping to simple expressions cannot depend on secret, which makes it possible to spare insecurity queries. As an example, let us perform RelSE of the toy program in Listing 1. Variable x is assigned a pair of expressions ⟨ |  ′ ⟩ and y is assigned a simple expression ⟨⟩. Note that the precondition that public variables are equal is now implicit since we use the same symbolic variable in both executions. At line 3, the conditional expression is evaluated to  = ⟨ ≠ 0⟩ and we need to check that the leakage of  is secure.
Challenge of binary-level analysis Recall that,Binsec/SE represents the memory as a special variable of type ( B 32 B 8 ). Consequently, it is not possible to directly store relational expressions in it. In order to store high inputs at the beginning of the execution, we have to duplicate it. In other words the memory is always duplicated. Consequently, every  operation will evaluate to a duplicated expression, preventing to spare queries in many situations. As an illustration, consider the compiled version of the previous program, given in Listing 2. The steps of RelSE on this program are given in Fig. 2. When the secret input is stored in memory at line 1, the array representing the memory is duplicated. This propagates to the load expression in eax at line 3 and to the conditional expression at line 4.
Intuitively, at line 4, eax should be equal to the simple expression ⟨⟩ in which case we could spare the insecurity query like in the previous example. However, because dependencies cannot be tracked in the array representing the memory, eax evaluates to a pair of  expression and we have to send the insecurity query to the solver. Practical impact. Table  1  reports the performance of constant-time analysis on an implementation of elliptic curve Curve25519-donna  [71]. Both SC and RelSE fail to prove the program secure in less than 1h. RelSE does reduce the number of queries compared to SC, but it is not sufficient. Our solution. To mitigate this issue, we propose dedicated simplifications for binary-level relational symbolic execution that allow a precise tracking of secret-dependencies in the memory (details in Section 5.
EXPERIMENTAL RESULTS Implementation. We implemented our relational symbolic execution, Binsec/Rel, on top of the binary-level analyzer Binsec  [56]. Binsec/Rel takes as input an x86 or ARM executable, a specification of high inputs and an initial memory configuration (possibly fully symbolic). It performs bounded exploration of the program under analysis (up to a usergiven depth), and reports identified violations together with counterexamples (i. e. , initial configurations leading to the vulnerabilities). In case no violation is reported, if the initial configuration is fully symbolic and the program has been explored exhaustively then the program is proven secure. Binsec/Rel is composed of a relational symbolic exploration module and an insecurity analysis module. The symbolic exploration module chooses the path to explore, updates the symbolic configuration, builds the path predicate and ensure that it is satisfiable.
The insecurity analysis module builds insecurity queries and ensures that they are not satisfiable. It can be configured according to the leakage model. We explore the program in a depth-first search manner and we rely on the Boolector SMT-solver  [76] , currently the best on theory QF_ABV  [77, 74]. Research questions. We investigate the following research questions: Setup. Experiments were performed on a laptop with an Intel(R) Core(TM) i5-2520M CPU @ 2. 50GHz processor and 32GB of RAM. Similarly to related work (e. g. [30] ), esp is initialized to a concrete value, we start the analysis from the beginning of the main function, we statically allocate data structures and the length of keys and buffers is fixed. When not stated otherwise, programs are compiled for a x86 (32bit) architecture with their default compiler setup.
Effectiveness of Binsec/Rel (RQ1) We carry out two experiments to assess the effectiveness of our technique: (1) bounded-verification of secure cryptographic primitives previously verified at source-or LLVM-level  [21, 22, 13]  (Section 6. 1. 1), (  2 ) automatic replay of known bug studies  [15, 22, 50]  (Section 6. 1. 2). Overall, our study encompasses 338 representative code samples for a total of 70k machine instructions and 22M unrolled instructions (i. e. , instructions explored by Binsec/Rel). 6. 1. 1 Bounded-Verification. We analyze a large range of secure constant-time cryptographic primitives (296 samples, 64k instructions), comprising: • Several basic constant-time utility functions such as selection functions  [15] , sort functions  [78]  and utility functions from HACL*  [13]  and OpenSSL  [79] , compiled with clang (versions 3.
0, 3. 9 and 7. 1), and gcc (versions 5. 4 and 8. 3) and for optimizations levels O0 and O3; • A set of representative constant-time cryptographic primitives already studied in the literature on source code  [21]  or LLVM  [22] , including implementations of TEA  [80] , Curve25519-donna  [71] , aes and des encryption functions taken from BearSSL  [81] , cryptographic primitives from libsodium  [12] , and the constant-time padding remove function tls-cbc-remove-padding, extracted from OpenSSL  [22] ; • A set of functions from the HACL* library  [13]. Results are reported in Table  2. For each program, Binsec/Rel is able to perform an exhaustive exploration without finding any violations of constant-time in less than 20 minutes. Note that exhaustive exploration is possible because in cryptographic programs, fixing the input size bounds loops.
Results are reported in Table  3  with fault-packing disabled to report vulnerabilities at the instruction level. All bugs have been found within the timeout. Interestingly, we found 3 unexpected binary-level vulnerabilities (from secure source codes) that slipped through prior analysis: • function ct_select_v1  [15]  was deemed secured through binary-level manual inspection, still we confirm that any version of clang with -O3 introduces a secret-dependent conditional jump which violates constant-time; • functions ct_sort and ct_sort_mult, verified by ct-verif  [22]  (LLVM bitcode compiled with clang), are vulnerable when compiled with gcc -O0 or clang -O3 -m32 -march=i386 (details in Section 6. 2).
Section 6. 4. 7). This accounts for a total of 1156 binaries and extends a prior manual study on scrubbing mechanisms  [18]. In this section, clang-all-versions (resp. gcc-all-versions) refer to all the aforementioned clang (resp. gcc) versions; and in tables ✓ indicates that a program is secure and ✗ that it is insecure w. r. t secret-erasure. 6. 4. 1 Naive implementations. First, we consider naive (insecure) implementations of scrubbing functions: • loop: naive scrubbing function that uses a simple for loop to set the memory to 0, TOPS, May, 2021, Lesly-Ann Daniel, Sébastien Bardin, and Tamara Rezk • memset: uses the memset function from the Standard C Library, • bzero: function defined in glibc to set memory to 0. clang-all-versions gcc-5. 4/6. 2/7. 2 gcc-8. 3/10. 2 clang-all-versions gcc-all-versions Results (cf.
Secondly, we observe that there are other factors that affect the preservation of secret-erasure. Indeed, the volatile_func program is still insecure because of register spilling. Additionally, loop and volatile_ptr_loop are also insecure because the loop is still optimized away. gcc-5. 4. 0 6. 2. 0 7. 2. 0 gcc-8. 3. 0 10. 2. 0 -O3 dse tdse both -O3 dse tdse both loop ✗ ✗ ✗ ✗ ✗ ✗ ✗ ✗ memset ✗ ✗ ✗ ✓ ✗ ✗ ✗ ✓ bzero ✗ ✓ ✗ ✓ ✗ ✗ ✗ ✓ explicit_bzero ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ memset_s ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ volatile_func ✗ ✗ ✗ ✗ ✗ ✗ ✗ ✗ ptr_to_volatile_loop ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ ptr_to_volatile_memset ✗ ✗ ✗ ✓ ✗ ✗ ✗ ✓ volatile_ptr_loop ✗ ✗ ✗ ✗ ✗ ✗ ✗ ✗ volatile_ptr_memset ✗ ✗ ✓ ✓ ✗ ✗ ✓ ✓ vol_ptr_to_vol_loop ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ vol_ptr_to_vol_memset ✗ ✗ ✓ ✓ ✗ ✗ ✓ ✓ memory_barrier_all (×4) ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ weak_symbols ✓ ✓ ✓ ✓ ✓ ✓ ✓ ✓ Table  11.
However, we did not encounter incomplete enumerations in our experiments: in the cryptographic primitives that we analyzed indirect jumps had a single (or few) target. Finally, any register or part of the memory that is concretized in the initial state of the symbolic execution might lead to unexplored program behaviors and missed violations. In Binsec/Rel, memory and register are symbolic by default and any concretization (e. g. setting the initial value of esp, or which memory addresses are initialized from the binary) must be made explicitly by the user. The definition of secret-erasure used in this paper is conservative in the sense that it forbids secret-dependent branches (and hence related implicit flows). We leave for future work the exploration of alternative (less conservative) definitions that could either declassify secret-dependent conditions, or allow secret-secret dependent conditions as long as both branches produce the same observations.
First, we consider the distinction between different views based on the importance of samples, and therefore apply a dynamic learning strategy for the automatic weighting of views and samples. Second, in the context of initializing binary clustering, we develop a new CNN feature and use a low-dimensional binary embedding by exploiting the efficient capabilities of Fourier mapping. Moreover, our approach simultaneously learns a joint discrete representation and performs direct clustering using a constrained binary matrix factorization; the optimization problem is perfectly solved in a unified learning model. Experimental results conducted on several challenging datasets demonstrate the effectiveness and superiority of the proposed approach over state-of-the-art methods in terms of accuracy, normalized mutual information, and purity.
The following are the main elements of our contribution: 1. To exploit the heterogeneity of data with multiple views, we introduce an automatically weighted strategy to control the pairwise importance of each sample and each view separately. View weights are implicitly derived from the square root of the view objective function, while sample weights are explicitly estimated. 2. We propose an objective function whose optimization allows the joint estimation of the following entities: the common binary code of the data, the two sets of weights, the view-based mapping from the nonlinear representation to the common binary code space, the binary centroids, and the cluster assignment matrix. 3. Deep features are extracted from the Vgg16 network to obtain a good initialization for the proposed optimization.
Related work Multi-view clustering (MVC) is an exciting topic in machine learning and has been explored using various strategies. Before diving into related work, we present an anthology of MVC methods. The fact that a considerable number of multi-view approaches can be classified into the following categories: Spectral Clustering  [12]  , Graph-based Clustering  [13]  , and Subspace Clustering  [14]. Here we briefly describe some interesting works: • RMSC  [15]  : This method started with the construction of a graph for each view. Then, according to the low-rank constraint and sparse decomposition, a joint transition probability matrix was used as the crucial input to the standard Markov chain method for clustering. This method is not suitable for large datasets. It overlooks the flexible structure of the local manifold, which cannot satisfy the agreement between views.
Anchor-based representation Considering an RBF (Radial Basis Function) that could evidently arrange different views into a single tensor with fixed dimensionality and well explore the high-order latent structure within multiple views by projecting them into a higher dimensional space. We consider a multi-view dataset consists of V representations (i. e. V views) for n instances, which are designated by a set of matrices { X 1 ,. , X V } ; where X v ∈ R d v ×n , is the data matrix of the v th view, and d v is the dimensionality of data features from the v th view. It is assumed that data samples in each view are zerocentered, i. e. s x v s = 0 , to maintain the balance of the data. The first step is to encode data using non-linear RBF mapping. This encoding is given by the following mapping: (x v s ) = exp - || x v s -a v 1 || 2 σ v ,.
, e xp - || x v s -a v m || 2 σ v T (1) where σ v is the kernel width for the v th view, (x v s ) ∈ R m represents m-dimensional non-linear embedding for the s th sample from the v th view, { a v 1 , a v 2 ,. , a v m } is a set of m selected anchors from v th view. One approach is to think of anchors as being statistically representative of that wider dataset. We get these anchors using the K -medoids technique, by leveraging its robustness to noise  [25]  , rather than random sampling or K-means. Remark: We fix the number of selected anchors for each view to m = 10 0 0 based on the outlined experiments in Zheng et al. [7]. It should also be noted that the influence of the kernel width parameter σ v is critical, as it determines the extent of smoothing  [26]  and often requires a lot of manual investigation.
Binary clustering initialization The solution to our iterative clustering problem depends heavily on the initial setup of the binary matrix to be factorized. The effect of an improper initialization is interpreted as the clustering algorithm getting stuck in a bad local minimum. Various Convolutional Neural Networks (CNN) architectures have been found to perform better than innovative hand-crafted feature detectors in detecting object features  [29]. Under this concept, we introduce new deep method called Bidirectional-Fast Fourier Transform "BD-FFT", which provides effective representative codes using Fourier decomposition  [24]. We use the rich feature representation of a pre-trained Visual Geometry Group model VGG16; the first task is to forward our image dataset and retrieve features from the second FC layer (4096 neurons).
Experimental setup 4. 1. 1. Datasets We perform experiments on four public multiview image datasets commonly used to benchmark clustering algorithms, including Caltech101-7, Caltech101-20 1 [32] , NUSWIDE-Obj 2  [33]  , and Scene-15 3 [34]. Multi-view features are extracted to describe each image. Table  2  exhibits a detailed description of these datasets. Caltech101 contains 9144 images grouped into 101 objects. By tracking the earlier work in Wang et al. [28]  , we select the frequently used object recognition dataset with 7 categories. 1474 images from the data are assembled to produce the so-called Caltech101-7. In addition, 2386 images affiliated with 20 classes are selected. This dataset is called Caltech101-20. Six different features were selected for both Caltech101-7 and Caltech101-20.
Parameter sensitivity The proposed model is parameterized so that its behavior can be tuned with three hyperparameters: β, γ , and λ. These regularization parameters are expected to contribute to a stable solution. We analyzed the effects of these parameters by setting λ to 1e -9 and empirically varying the values of β and γ from the grid {1e -5, 1e -4, 1e -3, 1e -2 1e -1 2, 4, 6, 10}. The variability of clustering accuracy for the four datasets and for different configurations of β and γ is shown in Fig. 2. We should mention here that the sensitivity across the Caltech101-7/20 datasets is also dependent on the number of selected anchors, which is recommended to be less than 10 0 0 anchors; this comes from the numerical perturbation, that will be addressed in the convergence analysis (section (4.
6) P. 30). We obtain excellent clustering performance when working with low values of β ( β = 1 e -5 ) and relatively high values of γ ( γ = 10 ). Clustering performance is relatively stable when 1 e -5 < β < 1 e -2 ; 2 < γ < 10 ; otherwise, we run the risk of losing effectiveness outside the optimal range. The summary of the best parameter setting for the three parameters is given in Table  3  , which shows that despite the sensitivity mentioned above, we obtained very good clustering results for all tested datasets with only one tuning of γ in a small search range.
Computational complexity In the proposed work, the problem of binary code learning was addressed as an interesting research approach to solve the problem of large-scale clustering of multiple views. The total complexity of AW-BMVC is O (nlm 2 V ) t when five optimization operations are considered: U v , B , C , G , W , and α,. This calculation goes beyond the complexity of deep feature extraction, which is a part of the preprocessing step. It can be observed that l n and m n where n is the number of data samples, and the small number of iterations "t", since the proposed model converges rapidly; consequently, the time complexity can be summarized to O (n ) , which depends linearly on n. We fulfill our running time experiments using Matlab R2019b on PC machine with 2. 39 GHz, i-5-2430M CPU and 6 GB RAM memory.
In Table  4  , we give the running time of the different methods on Caltech101-7. It can be seen that DiMSC (355. 77 s), OMSC (107. 55 s), LMVSC (135. 79 s), SMVSC (236. 32 s) and Co-FW-MVFCM (1864. 57 s) are relatively time-consuming methods (more than 100 s) compared to other approaches. As you can see from this table, our method achieves clustering results within 15. 23 s in only t = 3 iterations for the Caltech101-7 dataset, which is due to the self-weighted term of the sample that slightly increases the time cost. The AWP, WMSC and BMVC methods show better time efficiency, but our approach achieves the best clustering results.
Ablation study Our proposed method consists of three core modules: (Automatic sample weighting; Automatic view weighting; and Initialization of binary clustering). In Table  5  , we report the performance on two tested datasets when each module is removed or added. Note that the combination of these three indispensable components leads to the all-out proposal, whose dominance is evidenced by the bold results, while the removal of these components leads us back to the BMVC framework  [7]  (the first row in Table  5  ). We note that merging the two variants sample and view autoweighted without considering the binary clustering initialization part can result in a massive performance drop; accordingly, the BCI module plays an important role in improving the clustering performance. Furthermore, attempting to separate either auto-weighted component from the binary clustering initialization variant reduces the capacity of the model.
Clustering initialization analysis To further investigate the impact of different initialization scenarios of the binary codes on our proposed optimization algorithm, we conducted a group of experiments on all datasets. Algorithm 1 was used with three initialization scenarios for the matrix of binary codes B : A random binary matrix, non-linear PCA, and Deep-FFT. In the first scenario, we generate a random binary matrix; the second scenario shows a non-linear PCA technique adopted by the BMVC method  [7]  ; the third technique refers to Deep-FFT, which is our proposed initialization scenario. As can be seen in Table  6  , the obvious worst results are obtained by the binary random matrix, which is completely independent of the data. The non-linear PCA method exposes homogeneous but sub-optimal scoring metrics.
Convergence analysis Figure  3  shows the objective function value for each iteration on four datasets. The alternating iterative optimization strategy is used to iteratively update each variable: the mapping matrix U v , the discrete representation B , the binary cluster centroids C , the cluster indicator matrix G , the auto-weighted sample W , and the auto-weighted view α. The subproblems U v and B arising from Eqs. (  12 ) to (  14 ) guarantee a closed form optimal solutions given by Eqs. (  13 ) and  (15)  , respectively. The subproblem C in Eq. (  17 ) has an analytical solution using ADPLM  [10]  , Eq. (  20 ) effectively shows its optimal solution, followed by the obvious solution for G in Eq. (  21 ) , which is similar to the K-means learning scheme. The solution for the automatic weighting of samples in Eq.
(  29 ) as well as the automatic weighting of views in Eq. (  8 ) are the exact minimum points. As a result, the loss values of the globally adopted objective function F (U ; B ; C ; G ; W ; α) in Eq. (  11 ) decrease rapidly and reach the minimum point after about t = 5 iterations, along with verifying the monotonic bound, which is a sufficient condition for convergence. Numerical perturbation on Caltech101-7/20 Another phenomenon that may reveal the stability dilemma occurred when we experimented with the Caltech101-7/20 datasets in particular. A numerical perturbation occurred that resulted in a rapid and transient drop in the objective function to its minimum value. Subsequently, a sudden rise and/or stall was observed as the computation of the U v mapping matrices became ill-conditioned.