Vision Transformers (ViTs) and their variants have been increasingly adopted in intelligent systems. However, the security implications of partially exposing self-attention information in ViTs remain largely underexplored. Existing adversarial attacks on ViTs typically rely on white-box assumptions with unrealistic access or black-box settings with limited effectiveness, limiting their relevance to restricted deployment conditions. In this paper, we investigate a plausible gray-box threat model motivated by interpretability-oriented deployment scenarios, where limited attention-related information may be observable through interpretability or analysis interfaces. Our analysis suggests that such partial attention exposure may introduce a previously underexplored vulnerability in Vision Transformers. Based on this observation, we propose Targeted Patch Perturbation (TPP), an attention-guided patch perturbation framework tailored for restricted gray-box settings that localizes semantically important patches and restricts perturbations to these regions. The proposed method enables effective adversarial attacks without requiring gradient access to the target model during attack execution. Experiments on CIFAR-10, CIFAR-100, and ImageNet demonstrate that TPP consistently outperforms strong black-box baselines under the same perturbation budget. Further evaluations across multiple ViT architectures reveal that attention-guided patch selection can substantially improve attack transferability under restricted-information settings, suggesting that semantically aligned perturbation localization may affect shared semantic representations across transformer models and influence the adversarial robustness of Vision Transformer systems. The source code is available at: https://github.com/BaoChau-Ho/TGP_adv

Summary Handling hardware‐dependent properties at a low level is usually required in developing microcontroller‐based applications. One of these hardware‐dependent properties is cautions, which are described in microcontrollers hardware manuals. The process of verifying these cautions is performed manually, as there is currently no single tool that can directly handle this task. This research aims at automating the verification of these cautions. To obtain the typical cautions of microcontrollers, we investigate two sections which have a considerable number of required cautions in the hardware manual of a popular microcontroller. Subsequently, we analyse these cautions and categorize them into several groups. Based on this analysis, we propose a semi‐automatic approach for verifying the cautions which integrates two static programme analysis techniques (i.e., pattern matching and abstract interpretation). To evaluate our approach, we conducted experiments with generated source code, benchmark source code, and industrial source code. The generated source code, which was created automatically based on several aspects of the C programme, was used to evaluate the performance of the approach based on these aspects. The benchmark and the industrial source code, which were provided by Aisin Software Co., Ltd., were used to assess the feasibility and applicability of the approach. The results show that all expected violations in the benchmark source code were detected. Unexpected but real violations in the benchmark programme were also detected. For the industrial source code, the approach successfully handled and detected most of the expected violations. These results show that the approach is promising in verifying the cautions.

Microcontrollers are usually supplied with hardware manuals, where information that requires special attention is emphasized as cautions. Currently, the process of verifying these cautions is performed manually as there is no single tool that can directly handle this task. This research aims at automating the verification process for these cautions as much as possible. Firstly, we investigate two sections which have a considerable number of required cautions in the hardware manual of a popular microcontroller to obtain the typical cautions of microcontrollers. Secondly, we analyze and categorize these cautions into several groups. Subsequently, we propose a semi-automatic approach which uses the assertion-based method and integrates two existing static program analysis tools (i.e., Cobra and Eva plugin of Frama-C) to verify the cautions. To show the applicability of this approach, we conduct two experiments with a benchmark source code and an industrial source code provided by Aisin comCruise Co., Ltd.. The results show that this approach is capable of detecting all violations in the benchmark program and only misses one expected violation in the industrial project.

This document describes a practical experimentation of safety assessment of safety-critical software used in nuclear power plants. To enhance the credibility of safety assessments and to optimize the safety justification costs, the Research and Development Branch of Electicite de France (EDF) investigates the use of methods and tools for the semantic analysis of source code, so as to obtain indisputable proofs or so as to help assessors focus on the most critical points. Two tools based on different static analysis methods – Abstract Interpretation and Hoare Logic - were used for this experimentation. The use of two independent approaches is important since it confers a high level of confidence in the results. In addition, we found that the tools complement one another: the information provided by one tool was often used to improve the results of the other. We were able to prove formally that the application software of one of our shutdown systems is free from intrinsic run-time fault. The current versions of the tools were not mature enough for us to derive conclusions about the system software.