Biblio

Static analysis tools generate a large number of alarms that require manual inspection. In prior work, repositioning of alarms is proposed to (1) merge multiple similar alarms together and replace them by a fewer alarms, and (2) report alarms as close as possible to the causes for their generation. The premise is that the proposed merging and repositioning of alarms will reduce the manual inspection effort. To evaluate the premise, this paper presents an empirical study with 249 developers on the proposed merging and repositioning of static alarms. The study is conducted using static analysis alarms generated on \$C\$ programs, where the alarms are representative of the merging vs. non-merging and repositioning vs. non-repositioning situations in real-life code. Developers were asked to manually inspect and determine whether assertions added corresponding to alarms in \$C\$ code hold. Additionally, two spatial cognitive tests are also done to determine relationship in performance. The empirical evaluation results indicate that, in contrast to expectations, there was no evidence that merging and repositioning of alarms reduces manual inspection effort or improves the inspection accuracy (at times a negative impact was found). Results on cognitive abilities correlated with comprehension and alarm inspection accuracy.

This research aims to implement different modular exponentiation algorithms and evaluate the average complexity and compare it to the theoretical value. We use the library GMP to implement seven modular exponentiation algorithms. They are Left-to-right Square and Multiply, Right-to-left Square and Multiply, Left-to-right Signed Digit Square, and Multiply Left-to-right Square and Multiply Always Right-to-left Square and Multiply Always, Montgomery Ladder and Joye Ladder. For some exponent bit length, we choose 1024 bits and execute each algorithm on many exponent values and count the average numbers of squares and the average number of multiplications. Whenever relevant, our programs will check the consistency relations between the registers at the end of the exponentiation.

The biometric system of access to information resources has been developed. The software and hardware complex are designed to protect information resources and personal data from unauthorized access using the principle of user authentication by fingerprints. In the developed complex, the traditional input of login and password was replaced by applying a finger to the fingerprint scanner. The system automatically recognizes the fingerprint and provides access to the information resource, provides encryption of personal data and automation of the authorization process on the web resource. The web application was implemented using the Bootstrap framework, the 000webhost web server, the phpMyAdmin database server, the PHP scripting language, the HTML hypertext markup language, along with cascading style sheets and embedded scripts (JavaScript), which created a full-fledged web-site and Google Chrome extension with the ability to integrate it into other systems. The structural schematic diagram was performed. The design of the device is offered. The algorithm of the program operation and the program of the device operation in the C language are developed.

Today, large and complex software is developed with integrated components using application programming interfaces (APIs). Correct usage of APIs in practice presents a challenge due to implicit constraints, such as call conditions or call orders. API misuse, i.e., violation of these constraints, is a well-known source of bugs, some of which can cause serious security vulnerabilities. Although researchers have developed many API-misuse detectors over the last two decades, recent studies show that API misuses are still prevalent. In this paper, we provide a comprehensive empirical study on API-misuse bugs in open-source C programs. To understand the nature of API misuses in practice, we analyze 830 API-misuse bugs from six popular programs across different domains. For all the studied bugs, we summarize their root causes, fix patterns and usage statistics. Furthermore, to understand the capabilities and limitations of state-of-the-art static analysis detectors for API-misuse detection, we develop APIMU4C, a dataset of API-misuse bugs in C code based on our empirical study results, and evaluate three widely-used detectors on it qualitatively and quantitatively. We share all the findings and present possible directions towards more powerful API-misuse detectors.

Public key cryptography plays a vital role in many information and communication systems for secure data transaction, authentication, identification, digital signature, and key management purpose. Elliptic curve cryptography (ECC) is a widely used public key cryptographic algorithm. In this paper, we propose a hardware-software codesign implementation of the ECC cipher. The algorithm is modelled in C language. Compute-intensive components are identified for their efficient hardware implementations. In the implementation, residue number system (RNS) with projective coordinates are utilized for performing the required arithmetic operations. To manage the hardware-software codeign in an integrated fashion Xilinx platform studio tool and Virtex-5 xc5vfx70t device based platform is utilized. An application of the implementation is demonstrated for encryption of text and its respective decryption over prime fields. The design is useful for providing an adequate level of security for IoTs.

Software verification has been well applied in safety critical areas and has shown the ability to provide better quality assurance for modern software. However, as lines of code and complexity of software systems increase, the scalability of verification becomes a challenge. In this paper, we present an automatic software verification framework TSV to address the scalability issues: (i) the extended structural abstraction and property-guided program slicing to solve large-scale program verification problem, saving time and memory without losing accuracy; (ii) automatically select different verification methods according to the program and property context to improve the verification efficiency. For evaluation, we compare TSV's different configurations with existing C program verifiers based on open benchmarks. We found that TSV with auto-selection performs better than with bounded model checking only or with extended structural abstraction only. Compared to existing tools such as CMBC and CPAChecker, it acquires 10%-20% improvement of accuracy and 50%-90% improvement of memory consumption.

Creating and implementing fault-tolerant distributed algorithms is a challenging task in highly safety-critical industries. Using formal methods supports design and development of complex algorithms. However, formal methods are often perceived as an unjustifiable overhead. This paper presents the experience and insights when using TLA+ and PlusCal to model and develop fault-tolerant and safety-critical modules for TAS Control Platform, a platform for railway control applications up to safety integrity level (SIL) 4. We show how formal methods helped us improve the correctness of the algorithms, improved development efficiency and how part of the gap between model and implementation has been closed by translation to C code. Additionally, we describe how we gained trust in the formal model and tools by following a specific design process called property-driven design, which also implicitly addresses software quality metrics such as code coverage metrics.

The innovations in communication and computing technologies are changing the way we carry-out the tasks in our daily lives. These revolutionary and disrupting technologies are available to the users in various hardware form-factors like Smart Phones, Embedded Appliances, Configurable or Customizable add-on devices, etc. One such technology is Bluetooth [1], which enables the users to communicate and exchange various kinds of information like messages, audio, streaming music and file transfer in a Personal Area Network (PAN). Though it enables the user to carry-out these kinds of tasks without much effort and infrastructure requirements, they inherently bring with them the security and privacy concerns, which need to be addressed at different levels. In this paper, we present an application-layer framework, which provides strong mutual authentication of applications, data confidentiality and data integrity independent of underlying operating system. It can make use of the services of different Cryptographic Service Providers (CSP) on different operating systems and in different programming languages. This framework has been successfully implemented and tested on Android Operating System on one end (using Java language) and MS-Windows 7 Operating System on the other end (using ANSI C language), to prove the framework's reliability/compatibility across OS, Programming Language and CSP. This framework also satisfies the three essential requirements of Security, i.e. Confidentiality, Integrity and Availability, as per the NIST Guide to Bluetooth Security specification and enables the developers to suitably adapt it for different kinds of applications based on Bluetooth Technology.

Theft or loss of a mobile device could be an information security risk as it can result in loss of con fidential personal data. Traditional cryptographic algorithms are not suitable for resource constrained and handheld devices. In this paper, we have developed an efficient and user friendly tool called “NCRYPT” on Android platform. “NCRYPT” application is used to secure the data at rest on Android thus making it inaccessible to unauthorized users. It is based on lightweight encryption scheme i.e. Hummingbird-2. The application provides secure storage by making use of password based authentication so that an adversary cannot access the confidential data stored on the mobile device. The cryptographic key is derived through the password based key generation method PBKDF2 from the standard SUN JCE cryptographic provider. Various tools for encryption are available in the market which are based on AES or DES encryption schemes. Ihe reported tool is based on Hummingbird-2 and is faster than most of the other existing schemes. It is also resistant to most of attacks applicable to Block and Stream Ciphers. Hummingbird-2 has been coded in C language and embedded in Android platform with the help of JNI (Java Native Interface) for faster execution. This application provides choice for en crypting the entire data on SD card or selective files on the smart phone and protect p ersonal or confidential information available in such devices.

To instill greater confidence in computations outsourced to the cloud, clients should be able to verify the correctness of the results returned. To this end, we introduce Pinocchio, a built system for efficiently verifying general computations while relying only on cryptographic assumptions. With Pinocchio, the client creates a public evaluation key to describe her computation; this setup is proportional to evaluating the computation once. The worker then evaluates the computation on a particular input and uses the evaluation key to produce a proof of correctness. The proof is only 288 bytes, regardless of the computation performed or the size of the inputs and outputs. Anyone can use a public verification key to check the proof. Crucially, our evaluation on seven applications demonstrates that Pinocchio is efficient in practice too. Pinocchio's verification time is typically 10ms: 5-7 orders of magnitude less than previous work; indeed Pinocchio is the first general-purpose system to demonstrate verification cheaper than native execution (for some apps). Pinocchio also reduces the worker's proof effort by an additional 19-60x. As an additional feature, Pinocchio generalizes to zero-knowledge proofs at a negligible cost over the base protocol. Finally, to aid development, Pinocchio provides an end-to-end toolchain that compiles a subset of C into programs that implement the verifiable computation protocol.