-
Finding Software Vulnerabilities in Open-Source C Projects via Bounded Model Checking
Authors:
Janislley Oliveira de Sousa,
Bruno Carvalho de Farias,
Thales Araujo da Silva,
Eddie Batista de Lima Filho,
Lucas C. Cordeiro
Abstract:
Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an app…
▽ More
Computer-based systems have solved several domain problems, including industrial, military, education, and wearable. Nevertheless, such arrangements need high-quality software to guarantee security and safety as both are mandatory for modern software products. We advocate that bounded model-checking techniques can efficiently detect vulnerabilities in general software systems. However, such an approach struggles to scale up and verify extensive code bases. Consequently, we have developed and evaluated a methodology to verify large software systems using a state-of-the-art bounded model checker. In particular, we pre-process input source-code files and guide the respective model checker to explore them systematically. Moreover, the proposed scheme includes a function-wise prioritization strategy, which readily provides results for code entities according to a scale of importance. Experimental results using a real implementation of the proposed methodology show that it can efficiently verify large software systems. Besides, it presented low peak memory allocation when executed. We have evaluated our approach by verifying twelve popular open-source C projects, where we have found real software vulnerabilities that their developers confirmed.
△ Less
Submitted 9 November, 2023;
originally announced November 2023.
-
Asservissement visuel 3D direct dans le domaine spectral
Authors:
Maxime Adjigble,
Brahim Tamadazte,
Cristiana de Farias,
Rustam Stolkin,
Naresh Marturi
Abstract:
This paper presents a direct 3D visual servo scheme for the automatic alignment of point clouds (respectively, objects) using visual information in the spectral domain. Specifically, we propose an alignment method for 3D models/point clouds that works by estimating the global transformation between a reference point cloud and a target point cloud using harmonic domain data analysis. A 3D discrete…
▽ More
This paper presents a direct 3D visual servo scheme for the automatic alignment of point clouds (respectively, objects) using visual information in the spectral domain. Specifically, we propose an alignment method for 3D models/point clouds that works by estimating the global transformation between a reference point cloud and a target point cloud using harmonic domain data analysis. A 3D discrete Fourier transform (DFT) in $\mathbb{R}^3$ is used for translation estimation and real spherical harmonics in $SO(3)$ are used for rotation estimation. This approach allows us to derive a decoupled visual servo controller with 6 degrees of freedom. We then show how this approach can be used as a controller for a robotic arm to perform a positioning task. Unlike existing 3D visual servo methods, our method works well with partial point clouds and in cases of large initial transformations between the initial and desired position. Additionally, using spectral data (instead of spatial data) for the transformation estimation makes our method robust to sensor-induced noise and partial occlusions. Our method has been successfully validated experimentally on point clouds obtained with a depth camera mounted on a robotic arm.
△ Less
Submitted 3 April, 2023;
originally announced April 2023.
-
3D Spectral Domain Registration-Based Visual Servoing
Authors:
Maxime Adjigble,
Brahim Tamadazte,
Cristiana de Farias,
Rustam Stolkin,
Naresh Marturi
Abstract:
This paper presents a spectral domain registration-based visual servoing scheme that works on 3D point clouds. Specifically, we propose a 3D model/point cloud alignment method, which works by finding a global transformation between reference and target point clouds using spectral analysis. A 3D Fast Fourier Transform (FFT) in R3 is used for the translation estimation, and the real spherical harmon…
▽ More
This paper presents a spectral domain registration-based visual servoing scheme that works on 3D point clouds. Specifically, we propose a 3D model/point cloud alignment method, which works by finding a global transformation between reference and target point clouds using spectral analysis. A 3D Fast Fourier Transform (FFT) in R3 is used for the translation estimation, and the real spherical harmonics in SO(3) are used for the rotations estimation. Such an approach allows us to derive a decoupled 6 degrees of freedom (DoF) controller, where we use gradient ascent optimisation to minimise translation and rotational costs. We then show how this methodology can be used to regulate a robot arm to perform a positioning task. In contrast to the existing state-of-the-art depth-based visual servoing methods that either require dense depth maps or dense point clouds, our method works well with partial point clouds and can effectively handle larger transformations between the reference and the target positions. Furthermore, the use of spectral data (instead of spatial data) for transformation estimation makes our method robust to sensor-induced noise and partial occlusions. We validate our approach by performing experiments using point clouds acquired by a robot-mounted depth camera. Obtained results demonstrate the effectiveness of our visual servoing approach.
△ Less
Submitted 28 March, 2023;
originally announced March 2023.
-
Grasp Transfer for Deformable Objects by Functional Map Correspondence
Authors:
Cristiana de Farias,
Brahim Tamadazte,
Rustam Stolkin,
Naresh Marturi
Abstract:
Handling object deformations for robotic gras** is still a major problem to solve. In this paper, we propose an efficient learning-free solution for this problem where generated grasp hypotheses of a region of an object are adapted to its deformed configurations. To this end, we investigate the applicability of functional map (FM) correspondence, where the shape matching problem is treated as se…
▽ More
Handling object deformations for robotic gras** is still a major problem to solve. In this paper, we propose an efficient learning-free solution for this problem where generated grasp hypotheses of a region of an object are adapted to its deformed configurations. To this end, we investigate the applicability of functional map (FM) correspondence, where the shape matching problem is treated as searching for correspondences between geometric functions in a reduced basis. For a user selected region of an object, a ranked list of grasp candidates is generated with local contact moment (LoCoMo) based grasp planner. The proposed FM-based methodology maps these candidates to an instance of the object that has suffered arbitrary level of deformation. The best grasp, by analysing its kinematic feasibility while respecting the original finger configuration as much as possible, is then executed on the object. We have compared the performance of our method with two different state-of-the-art correspondence map** techniques in terms of grasp stability and region gras** accuracy for 4 different objects with 5 different deformations.
△ Less
Submitted 1 March, 2022;
originally announced March 2022.
-
SpectGRASP: Robotic Gras** by Spectral Correlation
Authors:
Maxime Adjigble,
Cristiana de Farias,
Rustam Stolkin,
Naresh Marturi
Abstract:
This paper presents a spectral correlation-based method (SpectGRASP) for robotic gras** of arbitrarily shaped, unknown objects. Given a point cloud of an object, SpectGRASP extracts contact points on the object's surface matching the hand configuration. It neither requires offline training nor a-priori object models. We propose a novel Binary Extended Gaussian Image (BEGI), which represents the…
▽ More
This paper presents a spectral correlation-based method (SpectGRASP) for robotic gras** of arbitrarily shaped, unknown objects. Given a point cloud of an object, SpectGRASP extracts contact points on the object's surface matching the hand configuration. It neither requires offline training nor a-priori object models. We propose a novel Binary Extended Gaussian Image (BEGI), which represents the point cloud surface normals of both object and robot fingers as signals on a 2-sphere. Spherical harmonics are then used to estimate the correlation between fingers and object BEGIs. The resulting spectral correlation density function provides a similarity measure of gripper and object surface normals. This is highly efficient in that it is simultaneously evaluated at all possible finger rotations in SO(3). A set of contact points are then extracted for each finger using rotations with high correlation values. We then use our previous work, Local Contact Moment (LoCoMo) similarity metric, to sequentially rank the generated grasps such that the one with maximum likelihood is executed. We evaluate the performance of SpectGRASP by conducting experiments with a 7-axis robot fitted with a parallel-jaw gripper, in a physics simulation environment. Obtained results indicate that the method not only can grasp individual objects, but also can successfully clear randomly organized groups of objects. The SpectGRASP method also outperforms the closest state-of-the-art method in terms of grasp generation time and grasp-efficiency.
△ Less
Submitted 26 July, 2021;
originally announced July 2021.
-
Dual Quaternion-Based Visual Servoing for Gras** Moving Objects
Authors:
Cristiana de Farias,
Maxime Adjigble,
Brahim Tamadazte,
Rustam Stolkin,
Naresh Marturi
Abstract:
This paper presents a new dual quaternion-based formulation for pose-based visual servoing. Extending our previous work on local contact moment (LoCoMo) based grasp planning, we demonstrate gras** of arbitrarily moving objects in 3D space. Instead of using the conventional axis-angle parameterization, dual quaternions allow designing the visual servoing task in a more compact manner and provide…
▽ More
This paper presents a new dual quaternion-based formulation for pose-based visual servoing. Extending our previous work on local contact moment (LoCoMo) based grasp planning, we demonstrate gras** of arbitrarily moving objects in 3D space. Instead of using the conventional axis-angle parameterization, dual quaternions allow designing the visual servoing task in a more compact manner and provide robustness to manipulator singularities. Given an object point cloud, LoCoMo generates a ranked list of grasp and pre-grasp poses, which are used as desired poses for visual servoing. Whenever the object moves (tracked by visual marker tracking), the desired pose updates automatically. For this, capitalising on the dual quaternion spatial distance error, we propose a dynamic grasp re-ranking metric to select the best feasible grasp for the moving object. This allows the robot to readily track and grasp arbitrarily moving objects. In addition, we also explore the robot null-space with our controller to avoid joint limits so as to achieve smooth trajectories while following moving objects. We evaluate the performance of the proposed visual servoing by conducting simulation experiments of gras** various objects using a 7-axis robot fitted with a 2-finger gripper. Obtained results demonstrate the efficiency of our proposed visual servoing.
△ Less
Submitted 16 July, 2021;
originally announced July 2021.
-
Simultaneous Tactile Exploration and Grasp Refinement for Unknown Objects
Authors:
Cristiana de Farias,
Naresh Marturi,
Rustam Stolkin,
Yasemin Bekiroglu
Abstract:
This paper addresses the problem of simultaneously exploring an unknown object to model its shape, using tactile sensors on robotic fingers, while also improving finger placement to optimise grasp stability. In many situations, a robot will have only a partial camera view of the near side of an observed object, for which the far side remains occluded. We show how an initial grasp attempt, based on…
▽ More
This paper addresses the problem of simultaneously exploring an unknown object to model its shape, using tactile sensors on robotic fingers, while also improving finger placement to optimise grasp stability. In many situations, a robot will have only a partial camera view of the near side of an observed object, for which the far side remains occluded. We show how an initial grasp attempt, based on an initial guess of the overall object shape, yields tactile glances of the far side of the object which enable the shape estimate and consequently the successive grasps to be improved. We propose a grasp exploration approach using a probabilistic representation of shape, based on Gaussian Process Implicit Surfaces. This representation enables initial partial vision data to be augmented with additional data from successive tactile glances. This is combined with a probabilistic estimate of grasp quality to refine grasp configurations. When choosing the next set of finger placements, a bi-objective optimisation method is used to mutually maximise grasp quality and improve shape representation during successive grasp attempts. Experimental results show that the proposed approach yields stable grasp configurations more efficiently than a baseline method, while also yielding improved shape estimate of the grasped object.
△ Less
Submitted 28 February, 2021;
originally announced March 2021.
-
Quadrupolar spin liquid, octupolar Kondo coupling and odd-frequency superconductivity in an exactly solvable model
Authors:
Carlene S. de Farias,
Vanuildo S. de Carvalho,
Eduardo Miranda,
Rodrigo G. Pereira
Abstract:
We propose an exactly solvable model for $j_{\text{eff}}=\frac32$ local moments on the honeycomb lattice. Our construction is guided by a symmetry analysis and by the requirement of an exact solution in terms of a Majorana fermion representation for multipole operators. The main interaction in the model can be interpreted as a bond-dependent quadrupole-quadrupole interaction. When time reversal sy…
▽ More
We propose an exactly solvable model for $j_{\text{eff}}=\frac32$ local moments on the honeycomb lattice. Our construction is guided by a symmetry analysis and by the requirement of an exact solution in terms of a Majorana fermion representation for multipole operators. The main interaction in the model can be interpreted as a bond-dependent quadrupole-quadrupole interaction. When time reversal symmetry is explicitly broken, we obtain a gapped spin liquid with a single chiral Majorana edge mode. We also investigate another solvable model in which the time-reversal-invariant spin liquid is coupled to conduction electrons in a superconductor. In the presence of a Kondo-like coupling that involves the octupole moment of the localized spins, the itinerant electrons hybridize with the emergent Majorana fermions in the spin liquid. This leads to spontaneous time reversal symmetry breaking and generates odd-frequency pairing. Our results suggest that $j_{\text{eff}}=\frac32$ systems with strong quadrupole-quadrupole interactions may provide a route towards non-Abelian quantum spin liquids and unconventional superconductivity.
△ Less
Submitted 12 August, 2020; v1 submitted 30 March, 2020;
originally announced March 2020.
-
MOEA/D with Uniformly Randomly Adaptive Weights
Authors:
Lucas R. C. de Farias,
Pedro H. M. Braga,
Hansenclever F. Bassani,
Aluizio F. R. Araújo
Abstract:
When working with decomposition-based algorithms, an appropriate set of weights might improve quality of the final solution. A set of uniformly distributed weights usually leads to well-distributed solutions on a Pareto front. However, there are two main difficulties with this approach. Firstly, it may fail depending on the problem geometry. Secondly, the population size becomes not flexible as th…
▽ More
When working with decomposition-based algorithms, an appropriate set of weights might improve quality of the final solution. A set of uniformly distributed weights usually leads to well-distributed solutions on a Pareto front. However, there are two main difficulties with this approach. Firstly, it may fail depending on the problem geometry. Secondly, the population size becomes not flexible as the number of objectives increases. In this paper, we propose the MOEA/D with Uniformly Randomly Adaptive Weights (MOEA/DURAW) which uses the Uniformly Randomly method as an approach to subproblems generation, allowing a flexible population size even when working with many objective problems. During the evolutionary process, MOEA/D-URAW adds and removes subproblems as a function of the sparsity level of the population. Moreover, instead of requiring assumptions about the Pareto front shape, our method adapts its weights to the shape of the problem during the evolutionary process. Experimental results using WFG41-48 problem classes, with different Pareto front shapes, shows that the present method presents better or equal results in 77.5% of the problems evaluated from 2 to 6 objectives when compared with state-of-the-art methods in the literature.
△ Less
Submitted 14 August, 2019;
originally announced August 2019.
-
Effective model for $A_{2g}$ Raman signal in URu$_2$Si$_2$
Authors:
Carlene Silva de Farias,
Marie-Aude Méasson,
Alvaro Ferraz,
Sébastien Burdin
Abstract:
We propose an effective model to describe the $A_{2g}$ signal in Raman scattering experiments in the URu$_{2}$Si$_{2}$ compound. We follow the scheme proposed earlier by Khveshchenko and Wiegmann [Phys. Rev. Lett. 73, 500 (1994)] to calculate the $A_{2g}$ scattering vertex. We extract the imaginary part of a two-point current-current correlation function and compare it directly with the Raman resp…
▽ More
We propose an effective model to describe the $A_{2g}$ signal in Raman scattering experiments in the URu$_{2}$Si$_{2}$ compound. We follow the scheme proposed earlier by Khveshchenko and Wiegmann [Phys. Rev. Lett. 73, 500 (1994)] to calculate the $A_{2g}$ scattering vertex. We extract the imaginary part of a two-point current-current correlation function and compare it directly with the Raman response. We obtain an inelastic peak at $A_{2g}$ channel owing to the interplay between a local staggered ordering and a possible quantum spin liquid behavior. Our results offer an explanation for the electronic Raman scattering experiments at the hidden order phase in URu$_{2}$Si$_{2}$ compound [Phys. Rev. Lett. 113, 266405 (2014)].
△ Less
Submitted 19 February, 2020; v1 submitted 24 October, 2017;
originally announced October 2017.
