Hamlen, Kevin W.

Permanent URI for this collectionhttps://hdl.handle.net/10735.1/6565

Kevin Hamlen is a Eugene McDermott Professor of Computer Science and a Senior Technical Advisor of UT Dallas' Cyber Security Research and Education Institute. His research focus is language-based security with the following research topics:

  • In-lined reference monitors
  • Type-safe intermediate languages
  • Abstract interpretation
  • Model-checking
  • Proof-carrying code
  • Certifying compilers
  • Software cyber-deception
  • Malware defense
  • Cloud computing security

Browse

Recent Submissions

Now showing 1 - 3 of 3
  • Item
    CUDA au Coq: A Framework for Machine-Validating GPU Assembly Programs
    (Institute of Electrical and Electronics Engineers Inc., 2019-03-25) Ferrell, Benjamin; Duan, Jun; Hamlen, Kevin W.; 50151836493420401232 (Hamlen, KW); Ferrell, Benjamin; Duan, Jun; Hamlen, Kevin W.
    A prototype framework for formal, machine-checked validation of GPU pseudo-assembly code algorithms using the Coq proof assistant is presented and discussed. The framework is the first to afford GPU programmers a reliable means of formally machine-validating high-assurance GPU computations without trusting any specific source-to-assembly compilation toolchain. A formal operational semantics for the PTX pseudo-assembly language is expressed as inductive, dependent Coq types, facilitating development of proofs and proof tactics that refer directly to the compiled PTX object code. Challenges modeling PTX's complex and highly parallelized computation model in Coq, with sufficient clarity and generality to tractably prove useful properties of realistic GPU programs, are discussed. Examples demonstrate how the prototype can already be used to validate some realistic programs. © 2019 EDAA.
  • Item
    Visualvital: An Observation Model for Multiple Sections of Scenes
    (Institute of Electrical and Electronics Engineers Inc.) Duan, Jun; Zhang, Kang; Hamlen, Kevin W.; 50151836493420401232 (Hamlen, KW); Duan, Jun; Zhang, Kang; Hamlen, Kevin
    A computational methodology for reorienting, repositioning, and merging camera positions within a region under surveillance is proposed, so as to optimally cover all features of interest without overburdening human or machine analysts with an overabundance of video information. This streamlines many video monitoring applications, such as vehicular traffic and security camera monitoring, which are often hampered by the difficulty of manually identifying the few specific locations (for tracks) or frames (for videos) relevant to a particular inquiry from a vast sea of hundreds or thousands of hours of video. VisualVital ameliorates this problem by considering geographic information to select ideal locations and orientations of camera positions to fully cover the span without losing key visual details. Given a target quantity of cameras, it merges relatively unimportant camera positions to reduce the quantity of video information that must be collected, maintained, and presented. Experiments apply the technique to paths chosen from maps of different cities around the world with various target camera quantities. The approach finds detail-optimizing positions with a time complexity of O(n log n). ©2017 IEEE.
  • Item
    Decentralized IoT Data Management Using BlockChain and Trusted Execution Environment
    (Institute of Electrical and Electronics Engineers Inc.) Ayoade, Ghadebo; Karande, Vishal; Khan, Latifur; Hamlen, Kevin W.; 51656251 (Khan, L); 50151836493420401232 (Hamlen, KW); Ayoade, Ghadebo; Karande, Vishal; Khan, Latifur; Hamlen, Kevin
    Due to the centralization of authority in the management of data generated by IoT devices, there is a lack of transparency in how user data is being shared among third party entities. With the popularity of adoption of blockchain technology, which provide decentralized management of assets such as currency as seen in Bitcoin, we propose a decentralized system of data management for IoT devices where all data access permission is enforced using smart contracts and the audit trail of data access is stored in the blockchain. With smart contracts applications, multiple parties can specify rules to govern their interactions which is independently enforced in the blockchain without the need for a centralized system. We provide a framework that store the hash of the data in the blockchain and store the raw data in a secure storage platform using trusted execution environment (TEE). In particular, we consider Intel SGX as a part of TEE that ensure data security and privacy for sensitive part of the application (code and data).

Works in Treasures @ UT Dallas are made available exclusively for educational purposes such as research or instruction. Literary rights, including copyright for published works held by the creator(s) or their heirs, or other third parties may apply. All rights are reserved unless otherwise indicated by the copyright owner(s).