Machine-based instruction editing

A method comprising:

• retrieving, by a processor from a data repository, a candidate source code that has been vetted for security, having a candidate function, and comprising a first human-readable machine instruction;
• accessing, by the processor from the data repository, a replacement function comprising a second human-readable machine instruction which has been previously identified as being preferred for security, wherein the replacement function comprises a set of instructions, that when converted to machine code, cause a machine to perform the replacement function;
• automatically determining, by the processor, equivalence between the candidate function and the replacement function, wherein the equivalence determination:
• derives a logic equation for the candidate function,
• accesses a logic equation for the replacement function,
• determines whether the logic equation for the candidate function and the logic equation for replacement function are logically equivalent by providing the logic equation for the candidate function and the logic equation for the replacement function to an automated theorem prover, and
• assesses whether given any input to the candidate function and the same input to the replacement function, an output value of the candidate function and output value for the replacement function are equal;
• upon equivalence being determined, automatically providing, by the processor, indicia of equivalence associated with the candidate function and the replacement function;
• upon the indicia being provided, automatically transforming, by the processor, the candidate source code comprising replacing the candidate function with the replacement function;
• and
• outputting the transformed candidate source code having preferred security features.

A system comprising:

• a memory;
• a processor;
• and
• wherein the processor:
• retrieves, from a data repository in the memory, a candidate source code that has been vetted for security, having a candidate function, and comprising a first human-readable machine instruction;
• accesses, from the data repository in the memory, a replacement function comprising a second human-readable machine instruction which has been previously identified as being preferred for security, wherein the replacement function comprises a set of instructions, that when converted to machine code, cause a machine to perform the replacement function;
• automatically determines equivalence between the candidate function and the replacement function, wherein the equivalence determination:
• derives a logic equation for the candidate function,
• accesses a logic equation for the replacement function,
• determines whether the logic equation for the candidate function and the logic equation for replacement function are logically equivalent by providing the logic equation for the candidate function and the logic equation for the replacement function to an automated theorem prover, and
• assesses whether given any input to the candidate function and the same input to the replacement function, an output value of the candidate function and output value for the replacement function are equal;
• upon equivalence being determined, automatically provides indicia of equivalence associated with the candidate function and the replacement function;
• upon the indicia being provided, automatically transforms the candidate source code comprising replacing the candidate function with the replacement function;
• and
• outputs the transformed candidate source code having preferred security features.

A computer-readable information storage media having stored thereon instructions, that when executed by one or more processors, cause to be performed a method comprising:

• retrieving, by a processor from a data repository, a candidate source code that has been vetted for security, having a candidate function, and comprising a first human-readable machine instruction;
• accessing, by the processor from the data repository, a replacement function comprising a second human-readable machine instruction which has been previously identified as being preferred for security, wherein the replacement function comprises a set of instructions, that when converted to machine code, cause a machine to perform the replacement function;
• automatically determining, by the processor, equivalence between the candidate function and the replacement function, wherein the equivalence determination:
• derives a logic equation for the candidate function,
• accesses a logic equation for the replacement function,
• determines whether the logic equation for the candidate function and the logic equation for replacement function are logically equivalent by providing the logic equation for the candidate function and the logic equation for the replacement function to an automated theorem prover, and
• assesses whether given any input to the candidate function and the same input to the replacement function, an output value of the candidate function and output value for the replacement function are equal;
• upon equivalence being determined, automatically providing, by the processor, indicia of equivalence associated with the candidate function and the replacement function;
• upon the indicia being provided, automatically transforming, by the processor, the candidate source code comprising replacing the candidate function with the replacement function;
• and
• outputting the transformed candidate source code having preferred security features.