43 research outputs found
Mosque at Mengda Township (Mengda xiang qingzhen si 孟達象清真寺)
No full textMengda 孟達 is a township (xiang 鄉) located on the south bank of the Yellow River (huang he 黃河), just on the western side of the Gorge of Piled Rocks (jishi xia 積石峽) that marked the traditional border between the Chinese-speaking loess farmlands and the Tibetan Plateau. The township is inhabited mainly by ethnic Salars (Ch. Sala zu 撒拉族), a small Turkic-speaking ethnicity that practices Islam. Explanatory plaques at the site claim that the mosque was originally built in the mid-Ming 明dynasty (1368-1644), and expanded in later centuries; while no Chinese-language inscriptions date the building, the styles of the murals inside seem to support this idea. As is common with many mosques in the region, the structure consists of an inner (western) chamber around the mihrab niche, and a larger outer (eastern) prayer hall. The inner hall is painted in tones of deep red, with Sini-script Arabic calligraphy in gold; the color-scheme suggests a probable Ming date. It appears that the outer hall was painted much later, probably in the nineteenth or early-twentieth centuries, with some individual panels added or recoloured in the 1990s or 2000s. Individual panels consist of landscape paintings (shanshui 山水), images of flower-vases or other auspicious objects, or trompe-l’œil images of hanging scrolls with Arabic calligraphy. Other images show calligraphic medallions placed on pedestals like Buddhist thrones, surrounded by halos of rainbow light (wuse guang 五色光). All of this suggests the vitality of Islamic mural-painting traditions in pre-Revolution China, and the close connections between this visual culture and the Han Chinese and Tibetan visual cultures surrounding it; these traditions are now largely lost elsewhere.Non UBCUnreviewedAuthor Affiliation: University of California, Berkeley, Qinghai Minzu UniversityGraduat
A Decision Procedure for String Logic with Quadratic Equations, Regular Expressions and Length Constraints
No full textIn this work, we consider the satisfiability problem in a logic that combines word equations over string variables denoting words of unbounded lengths, regular languages to which words belong and Presburger constraints on the length of words. We present a novel decision procedure over two decidable fragments that include quadratic word equations (i.e., each string variable occurs at most twice). The proposed procedure reduces the problem to solving the satisfiability in the Presburger arithmetic. The procedure combines two main components: (i) an algorithm to derive a complete set of all solutions of conjunctions of word equations and regular expressions; and (ii) two methods to precisely compute relational constraints over string lengths implied by the set of all solutions. We have implemented a prototype tool and evaluated it over a set of satisfiability problems in the logic. The experimental results show that the tool is effective and efficient
ABAC Requirements Engineering for Database Applications
No full textWe show how complex privacy requirements can be represented and processed by an extended model of Attribute Based Access Control (ABAC), working with a simple database applications pattern. During application model development, most likely based on UML (e.g. Use Case, Class Diagrams), the analyst and possibly the end user specifies ABAC permissions, and then verifies their effect by running queries on the target data. The ABAC model supports positive and negative permissions, “break glass” overrides of negative permissions, and message/alert generation. The permissions combining algorithms are based on relational database optimisation, and permissions processing is implemented by query modification, producing structurally-optimised queries in an SQL-like language; the queries can then be processed by many database and big data systems. The method and models have been implemented in a prototype Privacy Preferences Tool in collaboration with a large medical records development, and we discuss experiences with focus group evaluations of this tool
Towards a program logic for C11 release-sequences
No full textBy accepting order weakening for memory operations, the C11 memory model allows C/C++ programs to take advantage of modern hardware architectures, where weak/relaxed memory models are now the norm. However, the weakened C11 memory model introduces many complex and counterintuitive behaviours, rendering it more difficult for people to understand or reason about concurrent C11 programs. Several program logics (RSL, GPS, FSL, GPS+) have been proposed over the last few years to support formal reasoning for C11 programs, but each of them deals with only a specific subset of C11 programs, mainly due to the high complexity of the weakened memory model. Notably none of these program logics supports the reasoning of release-sequences-a highly flexible synchronisation mechanism in C11. Very recently, Doko and Vafeiadis propose a way in their FSL++ logic to reason about C11 programs using release-sequences, but their solution is restricted to those scenarios where only atomic update operations are between the release head and the receiver. In this paper we propose a new program logic that offers full support for reasoning about C11 programs using release-sequences. Our proposed logic is built on top of our previous program logic GPS+, but with much finer control over the resource transmission by introducing restricted-shareable assertions and an enhanced protocol system. We also illustrate our approach by verifying release-sequence programs that existing logics would not be able to.</p
A Program Logic for Reasoning About C11 Programs With Release-Sequences
No full textWith the popularity of weak/relaxed memory models widely used in modern hardware architectures, the C11 standard introduced a language level weak memory model, A.K.A the C11 memory model, that allows C/C++ programs to exploit the optimisation provided by the hardware platform in memory ordering and gain benefits in efficiency. On the other hand, with the weakened memory ordering allowed, more program behaviours are introduced, among which some are counterintuitive and make it even more challenging for programmers to understand or to formally reason about C11 multithread programs. To support the formal verification of the C11 weak memory programs, several program logics, e.g. RSL, GPS, FSL, and GPS+, have been developed during the last few years. However, due to the complexity of the weakened memory model, some intricate C11 features still cannot be handled in these logics. A notable example is the lack of supporting to the reasoning about a highly flexible C11 synchronisation mechanism, the release-sequence. Recently, the FSL++ logic proposed by Doko and Vafeiadis moves one step forward to address this problem, but FSL++ only considers the scenarios with atomic update operations in a release- sequence. In this article, we propose a new program logic, GPS++, that supports the reasoning about C11 programs with fully featured release-sequences. We also introduce fractional read permissions to GPS++, which are essential to the reasoning about a large number of real-world concurrent programs. GPS++ is a successor of our previous program logic GPS+, but it comes with much finer control over the resource transmission with the newly introduced restricted-shareable assertions and an enhanced protocol system. A more sophisticated resource model is devised to support the soundness proof of our new program logic. We also demonstrate GPS++ in action by verifying C11 programs with release-sequences that could not be handled by existing program logics
RetouchUAA: Unconstrained Adversarial Attack via Image Retouching
No full textDeep Neural Networks (DNNs) are susceptible to adversarial examples.
Conventional attacks generate controlled noise-like perturbations that fail to
reflect real-world scenarios and hard to interpretable. In contrast, recent
unconstrained attacks mimic natural image transformations occurring in the real
world for perceptible but inconspicuous attacks, yet compromise realism due to
neglect of image post-processing and uncontrolled attack direction. In this
paper, we propose RetouchUAA, an unconstrained attack that exploits a real-life
perturbation: image retouching styles, highlighting its potential threat to
DNNs. Compared to existing attacks, RetouchUAA offers several notable
advantages. Firstly, RetouchUAA excels in generating interpretable and
realistic perturbations through two key designs: the image retouching attack
framework and the retouching style guidance module. The former custom-designed
human-interpretability retouching framework for adversarial attack by
linearizing images while modelling the local processing and retouching
decision-making in human retouching behaviour, provides an explicit and
reasonable pipeline for understanding the robustness of DNNs against
retouching. The latter guides the adversarial image towards standard retouching
styles, thereby ensuring its realism. Secondly, attributed to the design of the
retouching decision regularization and the persistent attack strategy,
RetouchUAA also exhibits outstanding attack capability and defense robustness,
posing a heavy threat to DNNs. Experiments on ImageNet and Place365 reveal that
RetouchUAA achieves nearly 100\% white-box attack success against three DNNs,
while achieving a better trade-off between image naturalness, transferability
and defense robustness than baseline attacks
The eigenvector-eigenvalue identity for the quaternion matrix with its algorithm and computer program
No full textPeter Denton, Stephen Parke, Terence Tao and Xining Zhang [arxiv 2019]
presented a basic and important identity in linear commutative algebra,
so-called {\bf the eigenvector-eigenvalue identity} (formally named in [BAMS,
2021]), which is a convenient and powerful tool to succinctly determine
eigenvectors from eigenvalues. The identity relates the eigenvector component
to the eigenvalues of and the minor , which is formulated in an
elegant form as
In fact, it has been widely applied in various fields such as numerical
linear algebra, random matrix theory, inverse eigenvalue problem, graph theory,
neutrino physics and so on. In this paper, we extend the eigenvector-eigenvalue
identity to the quaternion division ring, which is non-commutative. A version
of eigenvector-eigenvalue identity for the quaternion matrix is established.
Furthermore, we give a new method and algorithm to compute the eigenvectors
from the right eigenvalues for the quaternion Hermitian matrix. A program is
designed to realize the algorithm to compute the eigenvectors. An open problem
ends the paper. Some examples show a good performance of the algorithm and the
program
