Biblio

Protecting the confidentiality of information manipulated by a computing system is one of the most important challenges facing today's cybersecurity community. A promising step toward conquering this challenge is to formally verify that the end-to-end behavior of the computing system really satisfies various information-flow policies. Unfortunately, because today's system software still consists of both C and assembly programs, the end-to-end verification necessarily requires that we not only prove the security properties of individual components, but also carefully preserve these properties through compilation and cross-language linking. In this paper, we present a novel methodology for formally verifying end-to-end security of a software system that consists of both C and assembly programs. We introduce a general definition of observation function that unifies the concepts of policy specification, state indistinguishability, and whole-execution behaviors. We show how to use different observation functions for different levels of abstraction, and how to link different security proofs across abstraction levels using a special kind of simulation that is guaranteed to preserve state indistinguishability. To demonstrate the effectiveness of our new methodology, we have successfully constructed an end-to-end security proof, fully formalized in the Coq proof assistant, of a nontrivial operating system kernel (running on an extended CompCert x86 assembly machine model). Some parts of the kernel are written in C and some are written in assembly; we verify all of the code, regardless of language.

With the advancement of Internet in Things (IoT) more and more "things" are connected to each other through the Internet. Due to the fact that the collected information may contain personal information of the users, it is very important to ensure the security of the devices in IoT. Diversification is a promising technique that protects the software and devices from harmful attacks and malware by making interfaces unique in each separate system. In this paper we apply diversification on the interfaces of IoT operating systems. To this aim, we introduce the diversification in post-compilation and linking phase of the software life-cycle, by shuffling the order of the linked objects while preserving the semantics of the code. This approach successfully prevents malicious exploits from producing adverse effects in the system. Besides shuffling, we also apply library symbol diversification method, and construct needed support for it e.g. into the dynamic loading phase. Besides studying and discussing memory layout shuffling and symbol diversification as a security measures for IoT operating systems, we provide practical implementations for these schemes for Thingsee OS and Raspbian operating systems and test these solutions to show the feasibility of diversification in IoT environments.

Different applications concurrently running on modern MPSoCs can interfere with each other when they use shared resources. This interference can cause side channels, i.e., sources of unintended information flow between applications. To prevent such side channels, we propose a hybrid mapping methodology that attempts to ensure spatial isolation, i.e., a mutually-exclusive allocation of resources to applications in the MPSoC. At design time and as a first step, we compute compact and connected application mappings (called shapes). In a second step, run-time management uses this information to map multiple spatially segregated shapes to the architecture. We present and evaluate a (fast) heuristic and an (exact) SAT-based mapper, demonstrating the viability of the approach.

Programming languages permitting immediate memory accesses through pointers often result in applications having memory-related errors, which may lead to unpredictable failures and security vulnerabilities. A light-weight solution is presented in this paper to tackle such illegal memory accesses dynamically in C/C++ based applications. We propose a new and effective method of instrumenting an application's source code at compile time in order to detect out-of-bound memory accesses. It is based on creating tags, to be coupled with each memory allocation and then placing additional tag checking instructions for each access made to the memory. The proposed solution is evaluated by instrumenting applications from the BugBench benchmark suite and publicly available benchmark software, Runtime Intrusion Prevention Evaluator (RIPE), detecting all the bugs successfully. The performance and memory overhead is further analysed by instrumenting and executing real world applications.

Providing efficient protection against energy consumption based side channel attacks (SCAs) for block ciphers is a relevant topic for the research community, as current overheads are in the 100x range. Unprofiled SCAs exploit information leakage from the outmost rounds of a cipher; we propose a solution encasing it between keyed transformations amenable to an efficient SCA protection. Our solution can be employed as a drop in replacement for an unprotected implementation, or be retrofit to an existing one, while retaining communication capabilities with legacy insecure endpoints. Experiments on a Cortex-M4 μC, show performance improvements in the range of 60x, compared with available solutions.

Side Channel Attacks (SCA) have proven to be a practical threat to the security of embedded systems, exploiting the information leakage coming from unintended channels concerning an implementation of a cryptographic primitive. Given the large variety of embedded platforms, and the ubiquity of the need for secure cryptographic implementations, a systematic and automated approach to deploy SCA countermeasures at design time is strongly needed. In this paper, we provide an overview of recent compiler-based techniques to protect software implementations against SCA, making them amenable to automated application in the development of secure-by-design systems.

Physical attacks especially fault attacks represent one the major threats against embedded systems. In the state of the art, software countermeasures against fault attacks are either applied at the source code level where it will very likely be removed at compilation time, or at assembly level where several transformations need to be performed on the assembly code and lead to significant overheads both in terms of code size and execution time. This paper presents the use of compiler techniques to efficiently automate the application of software countermeasures against instruction-skip fault attacks. We propose a modified LLVM compiler that considers our security objectives throughout the compilation process. Experimental results illustrate the effectiveness of this approach on AES implementations running on an ARM-based microcontroller in terms of security overhead compared to existing solutions.

Heap buffer overflow (underflow) errors are a common source of security vulnerabilities. One prevention mechanism is to add object bounds meta information and to instrument the program with explicit bounds checks for all memory access. The so-called "fat pointers" approach is one method for maintaining and propagating the meta information where native machine pointers are replaced with "fat" objects that explicitly store object bounds. Another approach is "low fat pointers", which encodes meta information within a native pointer itself, eliminating space overheads and also code compatibility issues. This paper presents a new low-fat pointer encoding that is fully compatible with existing libraries (e.g. pre-compiled libraries unaware of the encoding) and standard hardware (e.g. x86\_64). We show that our approach has very low memory overhead, and competitive with existing state-of-the-art bounds instrumentation solutions.

This poster documents three approaches that we are undertaking to increase security awareness within undergraduate computer science classes. The first approach is a verbal password entry system, with surreptitious photos being taken when the mobile device is stolen. The second approach is a lab where students develop a password entry and verification system between a mobile device and a remote server. The third approach is a captcha system, where students implement a simple challenge that can be verified. Like password entry, the captcha communications must be secure and difficult to automatically manipulate. Unlike password entry, the captcha is meant to allow humans access while denying other computers.

Text-based Captchas have been widely used to deter misuse of services on the Internet. However, many designs have been broken. It is intellectually interesting and practically relevant to look for alternative designs, which are currently a topic of active research. We motivate the study of Chinese Captchas as an interesting alternative design - co-unterintuitively, it is possible to design Chinese Captchas that are universally usable, even to those who have never studied Chinese language. More importantly, we ask a fundamental question: is the segmentation-resistance principle established for Roman-character based Captchas applicable to Chinese based designs? With deep learning techniques, we offer the first evidence that computers do recognize individual Chinese characters well, regardless of distortion levels. This suggests that many real-world Chinese schemes are insecure, in contrast to common beliefs. Our result offers an essential guideline to the design of secure Chinese Captchas, and it is also applicable to Captchas using other large-alphabet languages such as Japanese.

In this paper, we present an experimental system for controlling human access to information systems. Also, the system allows analyzing the morphology of red blood cells of microscope images of patients with sicklemia.

Three-dimensional typography (3D typography) refers to the arrangement of text in three-dimensional space. It injects vitality into the letters, thereby giving the viewer a strong impression that is hard to forget. These days, 3D typography plays an important role in daily life beyond the artistic design. It is easy to observe the 3D typography used in the 3D virtual space such as movie or games. Also it is used frequently in signboard or furniture design. Despite its noticeable strength, most of the 3D typography is generated by just a simple extrusion of flat 2D typography. Comparing with 2D typography, 3D typography is more difficult to generate in short time due to its high complexity.

While many text-based CAPTCHA schemes have been broken, hollow CAPTCHAs as a new technology have been used by many websites. The generation method of currently used hollow CAPTCHAs is investigated, we found there is color difference between the boundary of characters contour lines and noise arcs. An algorithm of noise arcs removal to deal with this vulnerability is proposed. Furthermore, a de-noising and segmentation scheme for hollow CAPTCHAs with noise arcs is presented. The scheme is verified by the real CAPTCHA data from the website Sina Weibo. The success segmentation rate is 77%. Finally, some advice is given to improve the design of hollow CAPTCHA.

Some of the common works like, upload and retrieval of data, buying and selling things, earning and donating or transaction of money etc., are the most common works performed in daily life through internet. For every user who is accessing the internet regularly, their highest priority is to make sure that there data is secured. Users are willing to pay huge amount of money to the service provider for maintaining the security. But the intention of malicious users is to access and misuse others data. For that they are using zombie bots. Always Bots are not the only malicious, legitimate authorized user can also impersonate to access the data illegally. This makes the job tougher to discriminate between the bots and boots. For providing security form that threats, here we are proposing a novel RSJ Approach by User Authentication. RSJ approach is a secure way for providing the security to the user form both bots and malicious users.

Accounts on web services are always exposed to the menace of attacks. Especially, a large number of accounts can be used for unfair uses such as stealth marketing or SPAM attacks. Needless to say, acquisition of those accounts and attacks are automatically done by software programs called bots. Therefore, a technology called CAPTCHA is usually used in the acquisition of accounts for web services in order to distinguish human beings from bots. The most popular kind of CAPTCHA methods is text-based CAPTCHA in which distorted alphabets and numbers appear with obstacles or noise. However, it is known that all of text-based CAPTCHA algorithms can be analyzed by computers. In addition, too much distortion or noise prevents human beings from alphabets or numbers. There are other kinds of CAPTCHA methods such as image CAPTCHA and audio CAPTCHA. However, they also have problems in use. As a related work, an effective text-based CAPTCHA algorithm was proposed to which amodal completion is applied. The CAPTCHA provides computers a large amount of calculation cost while amodal completion helps human beings to recognize characters momentarily. On the other hand, momentary recognition is uncomfortable for human beings since extreme concentration is required within ten seconds. Therefore, in this paper, we propose an improved algorithm to which amodal completion and aftereffects are applied. The aftereffects extend time for recognition of characters from a moment to several seconds.

Consider n anonymous nodes each initially supporting an opinion in \1, 2, …, k\ and suppose that they should all learn the opinion with the largest support. Per round, each node contacts a random other node and exchanges B bits with it, where typically B is at most O(log n). This basic distributed computing problem is called the plurality consensus problem (in the gossip model) and it has received extensive attention. An efficient plurality protocol is one that converges to the plurality consensus as fast as possible, and the standard assumption is that each node has memory at most polylogarithmic in n. The best known time bound is due to Becchetti et al. [SODA'15], reaching plurality consensus in O(k log n) rounds using log(k+1) bits of local memory, under some mild assumptions. As stated by Becchetti et al., achieving a poly-logarithmic time complexity remained an open question. Resolving this question, we present an algorithm that with high probability reaches plurality consensus in O(log k log n) rounds, while having message and memory size of log k + O (1) bits. This even holds under considerably more relaxed assumptions regarding the initial bias (towards plurality) compared to those of prior work. The algorithm is based on a very simple and arguably natural mechanism.

Advances in Device-to-Device (D2D) ecosystems have brought on mobile applications that utilise nearby mobile devices in order to improve users' quality of experience (QoE). The interactions between the mobile devices have to be transparent to the end users and can be of many services – opportunistic networking, traffic offloading, computation offloading, cooperative streaming and P2P based k-anonymity location privacy service, to name a few. Whenever mobile users are willing to "ask for help" from their neighbours, they need to make non trivial decisions in order to maximise their utility. Current motivation approaches for mobile users that participate in such environments are of two types: (i) credit-based and (ii) reputation-based. These approaches rely either on centralised authorities or require prohibitively many messages or require tamper resistant security modules. In this paper we propose a trust-based approach that does not require synchronisation between the mobile users. Moreover, we present the three-way tradeoff between, consistency, message exchange and awareness and we conclude that our approach can provide first-rate data to neighbour selection mechanisms for D2D ecosystems with much less overhead.

Digital Signage (DS) is one of the popular IoT technologies deployed in the urban space. DS can provide wayfinding and urban information to city dwellers and convey targeted messaging and advertising to people approaching the DS. With the rise of the online-to-offline (O2O) mobile commerce, DS also become an important marketing tool in urban retailing. However, most digital signage systems today lack interactive feature and context-aware recommendation engine. Few interactive digital signage systems available today are also insufficient in engaging anonymous viewers and also not considering temporal interaction between viewer and DS system. To overcome the above challenges, this paper proposes a context-aware recommender system framework with novel temporal interaction scheme for IoT based interactive digital signage deployed in urban space to engage anonymous viewer. The results of experiments indicate that the proposed framework improves the advertising effectiveness for DS system deployed in public in urban space.

Anonymous communication systems are vulnerable to long term passive "intersection attacks". Not all users of an anonymous communication system will be online at the same time, this leaks some information about who is talking to who. A global passive adversary observing all communications can learn the set of potential recipients of a message with more and more confidence over time. Nearly all deployed anonymous communication tools offer no protection against such attacks. In this work, we introduce TASP, a protocol used by an anonymous communication system that mitigates intersection attacks by intelligently grouping clients together into anonymity sets. We find that with a bandwidth overhead of just 8% we can dramatically extend the time necessary to perform a successful intersection attack.

This paper proposed a novel sparse representation-based infrared target tracking method using multi-feature fusion to compensate for incomplete description of single feature. In the proposed method, we extract the intensity histogram and the data on-Local Entropy and Local Contrast Mean Difference information for feature representation. To combine various features, particle candidates and multiple feature descriptors of dictionary templates were encoded as kernel matrices. Every candidate particle was sparsely represented as a linear combination of a set of atom vectors of a dictionary. Then, the sparse target template representation model was efficiently constructed using a kernel trick method. Finally, under the framework of particle filter the weights of particles were determined by sparse coefficient reconstruction errors for tracking. For tracking, a template update strategy employing Adaptive Structural Local Sparse Appearance Tracking (ASLAS) was implemented. The experimental results on benchmark data set demonstrate the better performance over many existing ones.

Person tracking is crucial in any automatic person surveillance systems. In this problem, person localization and re-identification (Re-ID) are both simultaneously processed to show separated trajectories for each individual. In this paper, we propose to use mixture of WiFi and camera systems for person tracking in indoor surveillance regions covered by WiFi signals and disjointed camera FOVs (Field of View). A fusion method is proposed to combine the position observations achieved from each single system of WiFi or camera. The combination is done based on an optimal assignment between the position observations and predicted states from camera and WiFi systems. The correction step of Kalman filter is then applied for each tracker to give out state estimations of locations. The fusion method allows tracking by identification in non-overlapping cameras, with clear identity information taken from WiFi adapter. The experiments on a multi-model dataset show outperforming tracking results of the proposed fusion method in comparison with vision-based only method.

Memory efficiency and locality have substantial impact on the performance of programs, particularly when operating on large data sets. Thus, memory- or I/O-efficient algorithms have received significant attention both in theory and practice. The widespread deployment of multicore machines, however, brings new challenges. Specifically, since the memory (RAM) is shared across multiple processes, the effective memory-size allocated to each process fluctuates over time. This paper presents techniques for designing and analyzing algorithms in a cache-adaptive setting, where the RAM available to the algorithm changes over time. These techniques make analyzing algorithms in the cache-adaptive model almost as easy as in the external memory, or DAM model. Our techniques enable us to analyze a wide variety of algorithms — Master-Method-style algorithms, Akra-Bazzi-style algorithms, collections of mutually recursive algorithms, and algorithms, such as FFT, that break problems of size N into subproblems of size Theta(Nc). We demonstrate the effectiveness of these techniques by deriving several results: 1. We give a simple recipe for determining whether common divide-and-conquer cache-oblivious algorithms are optimally cache adaptive. 2. We show how to bound an algorithm's non-optimality. We give a tight analysis showing that a class of cache-oblivious algorithms is a logarithmic factor worse than optimal. 3. We show the generality of our techniques by analyzing the cache-oblivious FFT algorithm, which is not covered by the above theorems. Nonetheless, the same general techniques can show that it is at most O(loglog N) away from optimal in the cache adaptive setting, and that this bound is tight. These general theorems give concrete results about several algorithms that could not be analyzed using earlier techniques. For example, our results apply to Fast Fourier Transform, matrix multiplication, Jacobi Multipass Filter, and cache-oblivious dynamic-programming algorithms, such as Longest Common Subsequence and Edit Distance. Our results also give algorithm designers clear guidelines for creating optimally cache-adaptive algorithms.

To increase transparency and interactive control in Recommender Systems, we extended the Matrix Factorization technique widely used in Collaborative Filtering by learning an integrated model of user-generated tags and latent factors derived from user ratings. Our approach enables users to manipulate their preference profile expressed implicitly in the (intransparent) factor space through explicitly presented tags. Furthermore, it seems helpful in cold-start situations since user preferences can be elicited via meaningful tags instead of ratings. We evaluate this approach and present a user study that to our knowledge is the most extensive empirical study of tag-enhanced recommending to date. Among other findings, we obtained promising results in terms of recommendation quality and perceived transparency, as well as regarding user experience, which we analyzed by Structural Equation Modeling.

In recent years, named entity linking (NEL) tools were primarily developed as general approaches, whereas today numerous tools are focusing on specific domains such as e.g. the mapping of persons and organizations only, or the annotation of locations or events in microposts. However, the available benchmark datasets used for the evaluation of NEL tools do not reflect this focalizing trend. We have analyzed the evaluation process applied in the NEL benchmarking framework GERBIL [16] and its benchmark datasets. Based on these insights we extend the GERBIL framework to enable a more fine grained evaluation and in deep analysis of the used benchmark datasets according to different emphases. In this paper, we present the implementation of an adaptive filter for arbitrary entities as well as a system to automatically measure benchmark dataset properties, such as the extent of content-related ambiguity and diversity. The implementation as well as a result visualization are integrated in the publicly available GERBIL framework.

Minutiae are important features in the fingerprints matching. The effective of minutiae extraction depends greatly on the results of fingerprint enhancement. This paper proposes a novel fingerprint enhancement method for direct gray scale extracting minutiae based on combining Gabor filters with the Adaptive Modified Finite Radon Transform (AMFRAT) filters. First, the proposed method uses Gabor filters as band-pass filters for deleting the noise and clarifying ridges. Next, AMFRAT filters are applied for connecting broken ridges together, filling the created holes and clarifying linear symmetry of ridges quickly. AMFRAT is the MFRAT filter, the window size of which is adaptively adjusted according to the coherence values. The small window size is for high curvature ridge areas (small coherence value), and vice versa. As the result, the ridges are the linear symmetry areas, and more suitable for direct gray scale minutiae extraction. Finally, linear symmetry filter is only used for locating minutiae in an inverse model, as "lack of linear symmetry" occurs at minutiae points. Experimental results on FVC2004 databases DB4 (set A) shows that the proposed method is capable of improving the goodness index (GI).