J Strother Moore

90 papers A* 7A 4B 8C 2Journal 35Unranked 27
YearRankTypeTitle / Venue / Authors
2025 conf
ACL2
Matt Kaufmann, J Strother Moore
2025 J jnl
Formal Aspects Comput.
J Strother Moore, Gordon D. Plotkin, David E. Rydeheard, Donald Sannella
2025 J jnl
CoRR
J Strother Moore, Gordon D. Plotkin, David E. Rydeheard, Donald Sannella
2024 ch.
The Practice of Formal Methods (I)
Matt Kaufmann, J Strother Moore
2023 conf
ACL2
Matt Kaufmann, J Strother Moore
2022 conf
ACL2
Warren A. Hunt Jr., Vivek Ramanathan, J Strother Moore
2020 conf
ACL2
Matt Kaufmann, J Strother Moore
2020 J jnl
J. Autom. Reason.
Matt Kaufmann, J Strother Moore
2019 J jnl
Formal Aspects Comput.
J Strother Moore
2017 J jnl
FLAP
J Strother Moore, Claus-Peter Wirth
2017 ch.
Provably Correct Systems
J Strother Moore
2017 conf
ARCADE@CADE
J Strother Moore, Marijn J. H. Heule
2015 B conf
ATVA
J Strother Moore
2015 conf
ACL2
J Strother Moore
2014 conf
ACL2
Matt Kaufmann, J Strother Moore
2014 B conf
ITP
J Strother Moore
2014 B conf
ITP
Matt Kaufmann, J Strother Moore
2013 J jnl
CoRR
J Strother Moore, Claus-Peter Wirth
2013 conf
ACL2
Matt Kaufmann, J Strother Moore
2012 J jnl
Dagstuhl Reports
Alan Bundy, Dieter Hutter, Cliff B. Jones, J Strother Moore
2012 A* conf
POPL
J Strother Moore
2011 conf
ACL2
Matt Kaufmann, J Strother Moore
2011 conf
PLPV
J Strother Moore
2011 B conf
FMCAD
J Strother Moore
2010 ch.
Design and Verification of Microprocessor Systems for High-Assurance Applications
Matt Kaufmann, J Strother Moore
2010 A* conf
LICS
J Strother Moore
2009 J jnl
J. Appl. Log.
Matt Kaufmann, J Strother Moore, Sandip Ray, Erik Reeber
2008 J jnl
J. Autom. Reason.
Sandip Ray, Warren A. Hunt Jr., John Matthews, J Strother Moore
2008 conf
TPHOLs
Matt Kaufmann, J Strother Moore
2008 A conf
SIGCSE
Robert B. Schnabel, Duncan A. Buell, Joanna Goode, J Strother Moore, Chris Stephenson
2008 J jnl
J. Funct. Program.
David A. Greve, Matt Kaufmann, Panagiotis Manolios, J Strother Moore, Sandip Ray, José-Luis Ruiz-Reina, Rob Sumners, Daron Vroon, Matthew Wilding
2008 J jnl
J. Autom. Reason.
Bishop Brock, Matt Kaufmann, J Strother Moore
2007 conf
ICSE Companion
Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2006 conf
UITP@FLoC
Peter C. Dillinger, Panagiotis Manolios, Daron Vroon, J Strother Moore
2006 conf
ACL2
Matt Kaufmann, J Strother Moore
2006 J jnl
Int. J. Softw. Tools Technol. Transf.
J Strother Moore
2006 B conf
LPAR
John Matthews, J Strother Moore, Sandip Ray, Daron Vroon
2005 conf
VSTTE
J Strother Moore
2005 J jnl
Sci. Comput. Program.
Hanbing Liu, J Strother Moore
2005 conf
TPHOLs
Warren A. Hunt Jr., Matt Kaufmann, Robert Bellarmine Krug, J Strother Moore, Eric Whitman Smith
2005 conf
TPHOLs
J Strother Moore, Qiang Zhang
2004 conf
TPHOLs
Hanbing Liu, J Strother Moore
2004 C conf
ICFEM
J Strother Moore
2004 B conf
FMCAD
Sandip Ray, J Strother Moore
2003 conf
IVME
Hanbing Liu, J Strother Moore
2003 conf
CHARME
J Strother Moore
2003 conf
CHARME
Warren A. Hunt Jr., Robert Bellarmine Krug, J Strother Moore
2003 J jnl
J. Autom. Reason.
Panagiotis Manolios, J Strother Moore
2002 conf
10th Anniversary Colloquium of UNU/IIST
J Strother Moore
2002 A conf
ICFP
J Strother Moore
2002 C conf
PADL
Robert S. Boyer, J Strother Moore
2002 J jnl
ACM Trans. Program. Lang. Syst.
J Strother Moore, George Porter
2001 conf
Java Virtual Machine Research and Technology Symposium
J Strother Moore, George Porter
2001 conf
TPHOLs
J Strother Moore
2001 J jnl
Inf. Process. Lett.
Panagiotis Manolios, J Strother Moore
2001 A* conf
CAV
J Strother Moore
2001 J jnl
J. Autom. Reason.
Matt Kaufmann, J Strother Moore
1999 J jnl
Formal Methods Syst. Des.
J Strother Moore
1999 conf
Correct System Design
J Strother Moore
1998 J jnl
IEEE Trans. Computers
J Strother Moore, Thomas W. Lynch, Matt Kaufmann
1998 book
A computational logic handbook, Second Edition.
Robert S. Boyer, J Strother Moore
1998 A* conf
CAV
J Strother Moore
1998 B conf
FMCAD
J Strother Moore
1997 J jnl
IEEE Trans. Software Eng.
Matt Kaufmann, J Strother Moore
1996 B conf
FMCAD
Bishop Brock, Matt Kaufmann, J Strother Moore
1994 J jnl
Formal Aspects Comput.
J Strother Moore
1994 J jnl
J. Autom. Reason.
J Strother Moore
1991 conf
Artificial and Mathematical Theory of Computation
Robert S. Boyer, David M. Goldschlag, Matt Kaufmann, J Strother Moore
1991 conf
Automated Reasoning: Essays in Honor of Woody Bledsoe
Robert S. Boyer, J Strother Moore
1990 A conf
CADE
Robert S. Boyer, J Strother Moore
1989 J jnl
J. Autom. Reason.
J Strother Moore
1989 J jnl
J. Autom. Reason.
William R. Bevier, Warren A. Hunt Jr., J Strother Moore, William D. Young
1988 J jnl
J. Autom. Reason.
Robert S. Boyer, J Strother Moore
1986 J jnl
ACM SIGSOFT Softw. Eng. Notes
Robert S. Boyer, J Strother Moore, Warren A. Hunt, Richard M. Cohen, Richard C. Holt
1986 A conf
CADE
Robert S. Boyer, J Strother Moore
1985 J jnl
ACM SIGSOFT Softw. Eng. Notes
Donald I. Good, Robert S. Boyer, J Strother Moore
1985 J jnl
J. Autom. Reason.
Robert S. Boyer, J Strother Moore
1984 J jnl
J. ACM
Robert S. Boyer, J Strother Moore
1983 J jnl
ACM SIGSOFT Softw. Eng. Notes
Robert S. Boyer, J Strother Moore
1980 book
A computational logic.
Robert S. Boyer, J Strother Moore
1979 J jnl
Inf. Process. Lett.
J Strother Moore
1979 book
A computational logic handbook.
Robert S. Boyer, J Strother Moore
1977 J jnl
Commun. ACM
Robert S. Boyer, J Strother Moore
1977 A* conf
IJCAI
Robert S. Boyer, J Strother Moore
1976 A* conf
POPL
Robert S. Boyer, J Strother Moore, Robert E. Shostak
1975 J jnl
SIGART Newsl.
J Strother Moore
1975 J jnl
IEEE Trans. Software Eng.
J Strother Moore
1975 J jnl
J. ACM
Robert S. Boyer, J Strother Moore
1973
J Strother Moore
1973 A* conf
IJCAI
Robert S. Boyer, J Strother Moore
redb/extractors/macho_extractor.py
← Index redb/extractors/macho_extractor.py python
import logging
from abc import ABCMeta, abstractmethod
import inspect
import sys
import os

import machofile

from redb.extractors.extractor import Extractor

logger = logging.getLogger(__name__)


@abstractmethod
class MachOExtractor(Extractor, metaclass=ABCMeta):

    def __init__(
        self,
        filepath,
        log,
        exporters=None,
        index_prefix=None,
        elastic_index=None,
        known_benign=False,
        known_malicious=False,
        macho=None,
    ):
        # Read binary and parse machofile BEFORE calling super().__init__
        # This avoids reading the file twice
        with open(filepath, "rb") as f:
            binary_data = f.read()

        # Parse machofile with binary data
        self.macho = macho if macho else self._generate_machofile_object(binary_data)

        # Extract hashes from machofile to pass to parent
        precomputed_hashes = None
        if self.macho:
            try:
                general_info = self.macho.get_general_info()
                if general_info:
                    # For FAT binaries, get_general_info() returns dict with 'fat' key
                    # For single-arch, it returns the info directly
                    if 'fat' in general_info:
                        fat_info = general_info['fat']
                        precomputed_hashes = {
                            'MD5': fat_info.get('MD5'),
                            'SHA1': fat_info.get('SHA1'),
                            'SHA256': fat_info.get('SHA256'),
                        }
                    else:
                        precomputed_hashes = {
                            'MD5': general_info.get('MD5'),
                            'SHA1': general_info.get('SHA1'),
                            'SHA256': general_info.get('SHA256'),
                        }
            except Exception as e:
                logger.debug(f"Could not get hashes from machofile: {e}")

        super().__init__(
            filepath,
            log,
            exporters,
            index_prefix,
            elastic_index,
            known_benign,
            known_malicious,
            precomputed_hashes=precomputed_hashes,
        )

        # Store binary data so base class doesn't re-read
        self._binary_data = binary_data

    @property
    def binary(self):
        """Override to use already-read binary data."""
        return self._binary_data

    def _generate_machofile_object(self, binary_data):
        """Generate and parse a machofile object from binary data."""
        macho = None
        try:
            macho = machofile.UniversalMachO(data=binary_data)
            if not macho:
                raise Exception("Empty file?")

            # Parse the MachO object once during initialization
            macho.parse()

        except Exception as e:
            logger.error(f"Format error parsing MachO: {e}")
        return macho

    # def _is_macho_file(self):
    #     """Check if the file is a valid Mach-O binary."""
    #     try:
    #         if not self.macho:
    #             return False
            
    #         # For Universal/FAT binaries, check if any architecture is valid
    #         if hasattr(self.macho, 'is_fat') and self.macho.is_fat:
    #             return len(self.macho.architectures) > 0
    #         else:
    #             # Single architecture binary
    #             return hasattr(self.macho, 'macho') and self.macho.macho is not None
    #     except Exception as e:
    #         self.log.error(f"Error checking Mach-O file: {e}")
    #         return False

    def _is_signed(self):
        """Check if the Mach-O binary is code signed using new API."""
        try:
            if not self.macho:
                return False

            # Get architectures using new API
            architectures = self.macho.get_architectures()

            # For each architecture, check if signed
            for arch in architectures:
                try:
                    signature_info = self.macho.get_code_signature_info(arch=arch)
                    if signature_info and signature_info.get('signed', False):
                        return True
                except Exception:
                    continue

            return False
        except Exception as e:
            self.log.error(f"Error checking Mach-O signature: {e}")
            return False

    def _get_architectures(self):
        """Get list of architectures in the Mach-O binary using new API."""
        try:
            if not self.macho:
                return []

            # Use new API method
            architectures = self.macho.get_architectures()
            return architectures if architectures else []
        except Exception as e:
            self.log.error(f"Error getting architectures: {e}")
            return []

    # def _get_macho_for_arch(self, arch_name=None):
    #     """Get MachO instance for specific architecture or default."""
    #     try:
    #         if not self.macho:
    #             return None
            
    #         if hasattr(self.macho, 'is_fat') and self.macho.is_fat:
    #             if arch_name:
    #                 return self.macho.architectures.get(arch_name)
    #             else:
    #                 # Return first available architecture
    #                 return next(iter(self.macho.architectures.values())) if self.macho.architectures else None
    #         else:
    #             # Single architecture binary
    #             return self.macho.macho if hasattr(self.macho, 'macho') else None
    #     except Exception as e:
    #         self.log.error(f"Error getting MachO for architecture: {e}")
    #         return None

    # def _get_formatted_header_values(self, header):
    #     """Get both raw and human-readable header values."""
    #     try:
    #         macho_instance = self._get_macho_for_arch()
    #         if not macho_instance:
    #             return None
            
    #         # Parse the MachO if not already parsed
    #         if not hasattr(macho_instance, 'header') or not macho_instance.header:
    #             macho_instance.parse()
            
    #         # Get human-readable values using machofile's formatting methods
    #         magic_str = macho_instance.format_magic_value(header.get('magic', 0))
            
    #         # Simple CPU type mapping since CPU_TYPE_MAP is not exposed
    #         cputype = header.get('cputype', 0)
    #         if cputype == 0x7:
    #             cputype_str = "x86"
    #         elif cputype == 0x1000007:
    #             cputype_str = "x86_64"
    #         elif cputype == 0xC:
    #             cputype_str = "ARM"
    #         elif cputype == 0x100000C:
    #             cputype_str = "ARM 64-bit"
    #         else:
    #             cputype_str = str(cputype)
            
    #         cpusubtype_str = macho_instance.decode_cpusubtype(header.get('cputype', 0), header.get('cpusubtype', 0))
    #         filetype_str = macho_instance.format_file_type(header.get('filetype', 0))
    #         flags_str = macho_instance.decode_flags(header.get('flags', 0))
            
    #         return {
    #             'raw': {
    #                 'magic': header.get('magic', 0),
    #                 'cputype': header.get('cputype', 0),
    #                 'cpusubtype': header.get('cpusubtype', 0),
    #                 'filetype': header.get('filetype', 0),
    #                 'flags': header.get('flags', 0),
    #             },
    #             'formatted': {
    #                 'magic_str': magic_str,
    #                 'cputype_str': cputype_str,
    #                 'cpusubtype_str': cpusubtype_str,
    #                 'filetype_str': filetype_str,
    #                 'flags_str': flags_str,
    #             }
    #         }
    #     except Exception as e:
    #         self.log.error(f"Error formatting header values: {e}")
    #         return None